set K = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #);
doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) is Subfield of F by lemug;
hence not SubFields F is empty by defX; :: thesis: SubFields F is Field-membered

now :: thesis: for x being object st x in SubFields F holds
x is Field

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

end;

hence SubFields F is Field-membered ; :: thesis: verum