A15: OrderedNAT is reflexive by Th44, ORDERS_2:def 2;
OrderedNAT is transitive by Th47, ORDERS_2:def 3;
hence OrderedNAT is quasi_ordered by A15, Def3; :: thesis: verum