:: deftheorem defX defines SubFields FIELD_12:def 13 :
for F being Field
for b₂ being set holds
( b₂ = SubFields F iff for o being object holds
( o in b₂ iff ex K being strict Field st
( o = K & K is Subfield of F ) ) );