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