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