now :: thesis: for x being object st x in { x where x is Element of F : for K being Subfield of F holds x in K } holds
x in the carrier of F

let x be object ; :: thesis: ( x in { x where x is Element of F : for K being Subfield of F holds x in K } implies x in the carrier of F )
assume x in { x where x is Element of F : for K being Subfield of F holds x in K } ; :: thesis: x in the carrier of F
then consider x1 being Element of F such that
A1: ( x1 = x & ( for K being Subfield of F holds x1 in K ) ) ;
thus x in the carrier of F by A1; :: thesis: verum

end;

hence { x where x is Element of F : for K being Subfield of F holds x in K } is Subset of F by TARSKI:def 3; :: thesis: verum