let r be Real; :: thesis: 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 ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( 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 ) ) )
assume A1: seq is bounded ; :: thesis: ( 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 ) )
hence ( r = lim_sup seq implies 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 ) ) by Th84, Th85; :: thesis: ( ( 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 ) ) implies r = lim_sup seq )
assume A2: 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 ) ; :: thesis: r = lim_sup seq
then for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ;
then A3: lim_sup seq <= r by A1, Th85;
for s being Real st 0 < s holds
for n being Nat ex k being Nat st seq . (n + k) > r - s by A2;
then r <= lim_sup seq by A1, Th84;
hence r = lim_sup seq by A3, XXREAL_0:1; :: thesis: verum