theorem Th19: :: PRE_POLY:20

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
[x,y] in R ) holds
(SgmX (R,A)) /. 1 = x