let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of 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 number st 0 < s holds
ex n being Element of NAT st
for k being Element of 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 number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
then A2: ( seq is bounded_below & seq is bounded_above ) ;
superior_realsequence seq is bounded by A1, Th58;
then A3: ( superior_realsequence seq is bounded_below & superior_realsequence seq is bounded_above ) ;
thus ( lim_sup seq <= r implies for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) :: thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) implies lim_sup seq <= r )

proof

assume A4: lim_sup seq <= r ; :: thesis: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s

proof

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
assume A5: 0 < s ; :: thesis: ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s

proof

consider n1 being Element of NAT such that
A6: (superior_realsequence seq) . n1 < (inf (superior_realsequence seq)) + s by A3, A5, Th8;
((superior_realsequence seq) . n1) + (inf (superior_realsequence seq)) < r + ((inf (superior_realsequence seq)) + s) by A4, A6, XREAL_1:10;
then ((superior_realsequence seq) . n1) + (inf (superior_realsequence seq)) < (r + s) + (inf (superior_realsequence seq)) ;
then A7: (((superior_realsequence seq) . n1) + (inf (superior_realsequence seq))) - (inf (superior_realsequence seq)) < r + s by XREAL_1:21;

now

let k be Element of NAT ; :: thesis: seq . (n1 + k) < r + s
seq . (n1 + k) <= (superior_realsequence seq) . n1 by A2, Th43;
then (seq . (n1 + k)) + ((superior_realsequence seq) . n1) < (r + s) + ((superior_realsequence seq) . n1) by A7, XREAL_1:10;
then ((seq . (n1 + k)) + ((superior_realsequence seq) . n1)) - ((superior_realsequence seq) . n1) < r + s by XREAL_1:21;
hence seq . (n1 + k) < r + s ; :: thesis: verum

end;

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

end;

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

end;

hence for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; :: thesis: verum

end;

assume A8: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; :: thesis: lim_sup seq <= r
for s being real number st 0 < s holds
lim_sup seq <= r + s

proof

let s be real number ; :: thesis: ( 0 < s implies lim_sup seq <= r + s )
assume A9: 0 < s ; :: thesis: lim_sup seq <= r + s
consider n1 being Element of NAT such that
A10: for k being Element of NAT holds seq . (n1 + k) < r + s by A8, A9;
for k being Element of NAT holds seq . (n1 + k) <= r + s by A10;
then A11: (superior_realsequence seq) . n1 <= r + s by A2, Th46;
inf (superior_realsequence seq) <= (superior_realsequence seq) . n1 by A3, Th8;
hence lim_sup seq <= r + s by A11, XXREAL_0:2; :: thesis: verum

end;

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