theorem Th9: :: JORDAN1H:9

for X being non empty set
for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A