theorem Th9: :: PRE_POLY:10

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