theorem Th7: :: SEQ_4:7

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