theorem :: DICKSON:50

NATOrd = RelIncl omega