for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) is one-to-one