:: deftheorem defines == FIELD_7:def 2 :
for F1, F2 being Field holds
( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );