theorem Th23: :: GAUSSINT:23

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