A15: OrderedNAT is reflexive by Th42;
OrderedNAT is transitive by Th45;
hence OrderedNAT is quasi_ordered by A15; :: thesis: verum