theorem :: LIOUVIL2:5

INT.Ring is Subring of F_Real by Th5, RING_3:47, ALGNUM_1:1;