theorem Th84: :: RINFSUP1:84

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