set A = RelStr(# X,O #);
field O = X by ORDERS_1:12;
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 2 :: thesis: verum