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