set A = TopRelStr(# X,O,T #);
A1: field the InternalRel of TopRelStr(# X,O,T #) = the carrier of TopRelStr(# X,O,T #) by ORDERS_1:12;
then A2: the InternalRel of TopRelStr(# X,O,T #) is_antisymmetric_in the carrier of TopRelStr(# X,O,T #) by RELAT_2:def 12;
( 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 #) ) by A1, RELAT_2:def 9, RELAT_2:def 16;
hence ( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric ) by A2; :: thesis: verum