theorem Th9: :: CHAIN_1:11

for X being non empty finite Subset of REAL ex ri being Element of REAL st
( ri in X & ( for xi being Real st xi in X holds
ri >= xi ) )