doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) == F ;
then reconsider K = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) as Subfield of F ;
F is Subfield of E by FIELD_4:7;
then A: K is Subfield of E by EC_PF_1:5;
( the addF of F = the addF of K || the carrier of F & the multF of F = the multF of K || the carrier of F & 1. F = 1. K & 0. F = 0. K ) by EC_PF_1:def 1;
then F is Subfield of K by EC_PF_1:def 1;
hence not IntermediateFields (E,F) is empty by A, defY; :: thesis: IntermediateFields (E,F) is Field-membered

now :: thesis: for x being object st x in IntermediateFields (E,F) holds
x is Field

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

end;

hence IntermediateFields (E,F) is Field-membered by FIELD_12:def 12; :: thesis: verum