theorem Th1: :: ARYTM_2:1

RAT+ c= REAL+ by Lm2, XBOOLE_1:7, XBOOLE_1:86;