theorem Th2: :: MESFUNC1:2

INT = INT- \/ NAT