:: deftheorem defines NATOrd DICKSON:def 14 :
NATOrd = { [x,y] where x, y is Element of NAT : x <= y } ;