theorem Th45: :: DICKSON:46

NATOrd is_transitive_in NAT