field R = X by ORDERS_1:15;
then R linearly_orders A by ORDERS_1:37, ORDERS_1:38;
hence ( not SgmX (R,A) is empty & SgmX (R,A) is one-to-one ) by Th9, Def2, RELAT_1:38; :: thesis: verum