<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
<OMS cd="logic1" name="implies"/>
<OMA>
<OMS cd="set1" name="in"/>
<OMV name="F"/>
<OMS cd="generic_alg_cats" name="field"/>
</OMA>
<OMA>
<OMS cd="set1" name="in"/>
<OMA>
<OMS cd="algebraic_cats" name="Abelian_group"/>
<OMA>
<OMS cd="algebraic_cats" name="field_set"/>
<OMV name="F"/>
</OMA>
<OMA>
<OMS cd="algebraic_cats" name="field_plus"/>
<OMV name="F"/>
</OMA>
<OMA>
<OMS cd="algebraic_cats" name="field_zero"/>
<OMV name="F"/>
</OMA>
<OMA>
<OMS cd="algebraic_cats" name="field_negative"/>
<OMV name="F"/>
</OMA>
</OMA>
<OMS cd="generic_alg_cats" name="Abelian_group"/>
</OMA>
</OMA>
</OMOBJ>
<math xmlns="http://www.w3.org/1998/Math/MathML">
<apply><csymbol cd="logic1">implies</csymbol>
<apply><csymbol cd="set1">in</csymbol><ci>F</ci><csymbol cd="generic_alg_cats">field</csymbol></apply>
<apply><csymbol cd="set1">in</csymbol>
<apply><csymbol cd="algebraic_cats">Abelian_group</csymbol>
<apply><csymbol cd="algebraic_cats">field_set</csymbol><ci>F</ci></apply>
<apply><csymbol cd="algebraic_cats">field_plus</csymbol><ci>F</ci></apply>
<apply><csymbol cd="algebraic_cats">field_zero</csymbol><ci>F</ci></apply>
<apply><csymbol cd="algebraic_cats">field_negative</csymbol><ci>F</ci></apply>
</apply>
<csymbol cd="generic_alg_cats">Abelian_group</csymbol>
</apply>
</apply>
</math>
set1.in($F, generic_alg_cats.field) ==> set1.in(algebraic_cats.Abelian_group(algebraic_cats.field_set($F), algebraic_cats.field_plus($F), algebraic_cats.field_zero($F), algebraic_cats.field_negative($F)), generic_alg_cats.Abelian_group)