theorem Th7: :: NUMBERS:7

NAT c< INT