theorem :: GAUSSINT:26

for K1 being strict Subfield of F_Rat holds K1 = F_Rat