theorem Th85: :: RINFSUP1:85

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