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