theorem Th15: :: CHORD:15

for p being non empty FinSequence
for T being non empty Subset of (rng p) ex x being set st
( x in T & ( for y being set st y in T holds
x .. p <= y .. p ) )