theorem Th5: :: SEQ_4:5

for X being real-membered set st not X is empty & X is bounded_above holds
ex g being Real st
( ( for r being Real st r in X holds
r <= g ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g - s < r ) ) )