:: deftheorem defines ExtNAT COUNTERS:def 1 :
ExtNAT = NAT \/ {+infty};