set a = the F -algebraic Element of E;
take T = { the F -algebraic Element of E}; :: thesis: ( not T is empty & T is finite & T is F -algebraic )
thus not T is empty ; :: thesis: ( T is finite & T is F -algebraic )
thus T is finite ; :: thesis: T is F -algebraic
for x being Element of E st x in T holds
x is F -algebraic by TARSKI:def 1;
hence T is F -algebraic by FIELD_7:def 12; :: thesis: verum