set M = { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } ;

now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
1. E in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies 1. E in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: 1. E in U
1. U = 1. E by EC_PF_1:def 1;
hence 1. E in U ; :: thesis: verum

end;

then A: 1. E in { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } ;

now :: thesis: for o being object st o in { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } holds
o in the carrier of E

let o be object ; :: thesis: ( o in { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } implies o in the carrier of E )
assume o in { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } ; :: thesis: o in the carrier of E
then consider x being Element of E such that
H: ( o = x & ( for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U ) ) ;
thus o in the carrier of E by H; :: thesis: verum

end;

hence { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } is non empty Subset of E by TARSKI:def 3, A; :: thesis: verum