theorem :: NUMBERS:27

NAT <> INT by Th7;