set M = { S where S is Subset of the carrier of F : ex K being strict Field st
( S = the carrier of K & K is Subfield of F ) } ;
defpred S₁[ object , object ] means ex K being strict Field st
( K = $2 & the carrier of K = $1 & K is Subfield of F );
A: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z by EC_PF_1:8;
consider A being set such that
B: for x being object holds
( x in A iff ex y being object st
( y in { S where S is Subset of the carrier of F : ex K being strict Field st
( S = the carrier of K & K is Subfield of F ) } & S₁[y,x] ) ) from TARSKI:sch 1(A);
take A ; :: thesis: for o being object holds
( o in A iff ex K being strict Field st
( o = K & K is Subfield of F ) )

C: now :: thesis: for x being object st x in A holds
ex K being strict Field st
( x = K & K is Subfield of F )

let x be object ; :: thesis: ( x in A implies ex K being strict Field st
( x = K & K is Subfield of F ) )
assume x in A ; :: thesis: ex K being strict Field st
( x = K & K is Subfield of F )
then consider y being object such that
D: ( y in { S where S is Subset of the carrier of F : ex K being strict Field st
( S = the carrier of K & K is Subfield of F ) } & S₁[y,x] ) by B;
consider K being strict Field such that
E: ( K = x & the carrier of K = y & K is Subfield of F ) by D;
thus ex K being strict Field st
( x = K & K is Subfield of F ) by E; :: thesis: verum

end;

now :: thesis: for x being object st ex K being strict Field st
( x = K & K is Subfield of F ) holds
x in A

let x be object ; :: thesis: ( ex K being strict Field st
( x = K & K is Subfield of F ) implies x in A )
assume ex K being strict Field st
( x = K & K is Subfield of F ) ; :: thesis: x in A
then consider K being strict Field such that
D: ( x = K & K is Subfield of F ) ;
the carrier of K c= the carrier of F by D, EC_PF_1:def 1;
then the carrier of K in { S where S is Subset of the carrier of F : ex K being strict Field st
( S = the carrier of K & K is Subfield of F ) } by D;
hence x in A by B, D; :: thesis: verum

end;

hence for o being object holds
( o in A iff ex K being strict Field st
( o = K & K is Subfield of F ) ) by C; :: thesis: verum