defpred S₁[ object ] means ex K being strict Field st
( K = $1 & F is Subfield of K );
consider A being set such that
A1: for x being object holds
( x in A iff ( x in SubFields E & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for x being object holds
( x in A iff ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) )

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

let x be object ; :: thesis: ( x in A implies ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) )
assume x in A ; :: thesis: ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E )
then A3: ( x in SubFields E & S₁[x] ) by A1;
then consider K being strict Field such that
A4: ( x = K & K is Subfield of E ) by FIELD_12:def 13;
thus ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) by A3, A4; :: thesis: verum

end;

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

let x be object ; :: thesis: ( ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) implies x in A )
assume A3: ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) ; :: thesis: x in A
then x in SubFields E by FIELD_12:def 13;
hence x in A by A1, A3; :: thesis: verum

end;

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