:: deftheorem defines INT NUMBERS:def 4 :
INT = (NAT \/ [:{0},NAT:]) \ {[0,0]};