let F, K be Field; :: thesis: ( K = PrimeField F iff ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) )
now :: thesis: ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) implies K = PrimeField F )
assume A1: ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) ; :: thesis: K = PrimeField F
then PrimeField F is Subfield of K by Th90;
hence K = PrimeField F by A1; :: thesis: verum
end;
hence ( K = PrimeField F iff ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) ) by Th89; :: thesis: verum