for F, K being Field holds
( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) )