theorem :: RINFSUP1:83

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
( ( for n being Nat ex k being Nat st seq . (n + k) < r + s ) & ex n being Nat st
for k being Nat holds r - s < seq . (n + k) ) )