theorem :: NUMBERS:28

NAT <> RAT by Th4, Th7;