theorem Th8: :: NUMBERS:8

NAT c< RAT by Th4, Th7, XBOOLE_1:56;