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