let F be Field; :: thesis: for E being FieldExtension of F
for K being strict Field holds
( K in IntermediateFields (E,F) iff ( F is Subfield of K & K is Subfield of E ) )
let E be FieldExtension of F; :: thesis: for K being strict Field holds
( K in IntermediateFields (E,F) iff ( F is Subfield of K & K is Subfield of E ) )
let K be strict Field; :: thesis: ( K in IntermediateFields (E,F) iff ( F is Subfield of K & K is Subfield of E ) )

now :: thesis: ( K in IntermediateFields (E,F) implies ( F is Subfield of K & K is Subfield of E ) )

assume K in IntermediateFields (E,F) ; :: thesis: ( F is Subfield of K & K is Subfield of E )
then consider K1 being strict Field such that
A: ( K1 = K & F is Subfield of K1 & K1 is Subfield of E ) by defY;
thus ( F is Subfield of K & K is Subfield of E ) by A; :: thesis: verum

end;

hence ( K in IntermediateFields (E,F) iff ( F is Subfield of K & K is Subfield of E ) ) by defY; :: thesis: verum