let F, K be Field; :: thesis: ( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) )

now :: thesis: ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) implies K = PrimeField F )

assume A1: ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) ; :: thesis: K = PrimeField F
then A2: ( the carrier of K c= the carrier of F & the addF of K = the addF of F || the carrier of K & the multF of K = the multF of F || the carrier of K & 1. F = 1. K & 0. F = 0. K ) by EC_PF_1:def 1;

A3: now :: thesis: for x being object st x in carrier/\ F holds
x in the carrier of K

let x be object ; :: thesis: ( x in carrier/\ F implies x in the carrier of K )
assume x in carrier/\ F ; :: thesis: x in the carrier of K
then consider y being Element of F such that
A4: ( x = y & ( for E being Subfield of F holds y in E ) ) ;
x in K by A4, A1;
hence x in the carrier of K ; :: thesis: verum

end;

now :: thesis: for x being object st x in the carrier of K holds
x in carrier/\ F

let x be object ; :: thesis: ( x in the carrier of K implies x in carrier/\ F )
assume A5: x in the carrier of K ; :: thesis: x in carrier/\ F
for E being Subfield of F holds x in E

proof

let E be Subfield of F; :: thesis: x in E
K is Subfield of E by A1;
then the carrier of K c= the carrier of E by EC_PF_1:def 1;
hence x in E by A5; :: thesis: verum

end;

hence x in carrier/\ F by A2, A5; :: thesis: verum

end;

then the carrier of K = carrier/\ F by A3, TARSKI:2;
hence K = PrimeField F by A1, A2, Def10; :: thesis: verum

end;

hence ( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) ) by Th90; :: thesis: verum