theorem Th4: :: EC_PF_1:4

for K1, K2 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K1 holds
K1 = K2