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