field R = X by ORDERS_1:100;
then R linearly_orders A by ORDERS_1:133, ORDERS_1:134;
hence ( not SgmX R,A is empty & SgmX R,A is one-to-one ) by RELAT_1:60, Th8T, Def2T; :: thesis: verum