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