:: deftheorem defines OrderedNAT DICKSON:def 15 :
OrderedNAT = RelStr(# NAT,NATOrd #);