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 ) )