for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
len (SgmX (R,A)) = card A