:: deftheorem defFm defines Field-membered FIELD_12:def 12 :
for X being set holds
( X is Field-membered iff for x being object st x in X holds
x is Field );