theorem Th89: :: RING_3:90

for F being Field
for E being strict Subfield of PrimeField F holds E = PrimeField F