set IntRel = the InternalRel of TrivAsymOrthoRelStr ;
the InternalRel of TrivAsymOrthoRelStr is_transitive_in {{} } by Th12;
hence TrivAsymOrthoRelStr is transitive by CARD_1:87, ORDERS_2:def 5; :: thesis: verum