theorem Th18: :: NUMBERS:18

NAT c= RAT by Th8;