theorem Th5: :: LIOUVIL2:4

F_Rat is Subring of F_Real by GAUSSINT:14, RING_3:43;