theorem :: RING_3:47

INT.Ring is Subring of F_Rat by Lm4, C0SP1:def 3;