let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F holds IntermediateFields (E,F) c= IntermediateFields (K,F)
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F holds IntermediateFields (E,F) c= IntermediateFields (K,F)
let K be F -extending FieldExtension of F; :: thesis: IntermediateFields (E,F) c= IntermediateFields (K,F)

now :: thesis: for o being object st o in IntermediateFields (E,F) holds
o in IntermediateFields (K,F)

let o be object ; :: thesis: ( o in IntermediateFields (E,F) implies o in IntermediateFields (K,F) )
assume o in IntermediateFields (E,F) ; :: thesis: o in IntermediateFields (K,F)
then consider U being strict Field such that
A: ( U = o & F is Subfield of U & U is Subfield of E ) by defY;
E is Subfield of K by FIELD_4:7;
then U is Subfield of K by A, EC_PF_1:5;
hence o in IntermediateFields (K,F) by A, defY; :: thesis: verum

end;

hence IntermediateFields (E,F) c= IntermediateFields (K,F) ; :: thesis: verum