set IntRel = the InternalRel of TrivAsymOrthoRelStr;
the InternalRel of TrivAsymOrthoRelStr is_transitive_in {{}} by PARTIT_2:26;
hence TrivAsymOrthoRelStr is transitive by CARD_1:49, ORDERS_2:def 3; :: thesis: verum