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