theorem Th9: :: NUMBERS:9

NAT c< REAL by Th2, Th8, XBOOLE_1:56;