theorem Th8: :: RINFSUP1:8

for r being Real
for seq being Real_Sequence st seq is bounded_below holds
( r = lower_bound seq iff ( ( for n being Nat holds r <= seq . n ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . k < r + s ) ) )