:: deftheorem defY defines IntermediateFields FIELD_14:def 1 :
for F being Field
for E being FieldExtension of F
for b₃ being set holds
( b₃ = IntermediateFields (E,F) iff for x being object holds
( x in b₃ iff ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) ) );