set A = RelStr(# X,O #);
field O = X by ORDERS_1:12;
hence the InternalRel of RelStr(# X,O #) is_transitive_in the carrier of RelStr(# X,O #) by RELAT_2:def 16; :: according to ORDERS_2:def 3 :: thesis: verum