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