set A = TopRelStr(# X,O,T #);
field the InternalRel of TopRelStr(# X,O,T #) = the carrier of TopRelStr(# X,O,T #) by ORDERS_1:97;
then ( the InternalRel of TopRelStr(# X,O,T #) is_reflexive_in the carrier of TopRelStr(# X,O,T #) & the InternalRel of TopRelStr(# X,O,T #) is_transitive_in the carrier of TopRelStr(# X,O,T #) & the InternalRel of TopRelStr(# X,O,T #) is_antisymmetric_in the carrier of TopRelStr(# X,O,T #) ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
hence ( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric ) by ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: verum