theorem Th20: :: PRE_POLY:21

for X being non empty set
for A being non empty finite Subset of X
for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX (R,A)) /. (len (SgmX (R,A))) = x