theorem Th25: :: GAUSSINT:25

for K1 being Subfield of F_Rat holds the carrier of K1 = the carrier of F_Rat