theorem Th90: :: RING_3:91

for F being Field
for E being Subfield of F holds PrimeField F is Subfield of E