theorem Th42: :: DICKSON:43

NATOrd is_reflexive_in NAT ;