theorem Th82: :: RINFSUP1:82

for r being Real
for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds r - s < seq . (n + k) )