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 Th10, Def2, RELAT_1:60; :: thesis: verum