let r be Real; :: thesis: 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 )
let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( 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 ) )
set seq1 = superior_realsequence seq;
assume A1: seq is bounded ; :: thesis: ( 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 )
then A2: superior_realsequence seq is bounded by Th56;
thus ( lim_sup seq <= r implies for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ) :: thesis: ( ( for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ) implies lim_sup seq <= r )

proof

assume A3: lim_sup seq <= r ; :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s
for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for k being Nat holds seq . (n + k) < r + s )
assume A4: 0 < s ; :: thesis: ex n being Nat st
for k being Nat holds seq . (n + k) < r + s
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s

proof

consider n1 being Nat such that
A5: (superior_realsequence seq) . n1 < (lower_bound (superior_realsequence seq)) + s by A2, A4, Th8;
((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < r + ((lower_bound (superior_realsequence seq)) + s) by A3, A5, XREAL_1:8;
then ((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < (r + s) + (lower_bound (superior_realsequence seq)) ;
then A6: (((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq))) - (lower_bound (superior_realsequence seq)) < r + s by XREAL_1:19;

now :: thesis: for k being Nat holds seq . (n1 + k) < r + s

let k be Nat; :: thesis: seq . (n1 + k) < r + s
seq . (n1 + k) <= (superior_realsequence seq) . n1 by A1, Th41;
then (seq . (n1 + k)) + ((superior_realsequence seq) . n1) < (r + s) + ((superior_realsequence seq) . n1) by A6, XREAL_1:8;
then ((seq . (n1 + k)) + ((superior_realsequence seq) . n1)) - ((superior_realsequence seq) . n1) < r + s by XREAL_1:19;
hence seq . (n1 + k) < r + s ; :: thesis: verum

end;

hence ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ; :: thesis: verum

end;

hence ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ; :: thesis: verum

end;

hence for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ; :: thesis: verum

end;

assume A7: for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ; :: thesis: lim_sup seq <= r
for s being Real st 0 < s holds
lim_sup seq <= r + s

proof

let s be Real; :: thesis: ( 0 < s implies lim_sup seq <= r + s )
assume 0 < s ; :: thesis: lim_sup seq <= r + s
then consider n1 being Nat such that
A8: for k being Nat holds seq . (n1 + k) < r + s by A7;
for k being Nat holds seq . (n1 + k) <= r + s by A8;
then A9: (superior_realsequence seq) . n1 <= r + s by A1, Th44;
lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n1 by A2, Th8;
hence lim_sup seq <= r + s by A9, XXREAL_0:2; :: thesis: verum

end;

hence lim_sup seq <= r by XREAL_1:41; :: thesis: verum