theorem Th91: :: RING_3:92

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