let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )
let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) )
set seq1 = superior_realsequence seq;
assume A1: seq is bounded ; :: thesis: ( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st 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 ( r <= lim_sup seq implies for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) :: thesis: ( ( for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) implies r <= lim_sup seq )

proof

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

proof

let n be Element of NAT ; :: thesis: ex k being Element of NAT st seq . (n + k) > r - s
consider k being Element of NAT such that
A6: seq . (n + k) > ((superior_realsequence seq) . n) - s by A2, A5, Th43;
(superior_realsequence seq) . n >= r by A3, A4, Th10;
then ((superior_realsequence seq) . n) + (seq . (n + k)) > r + (((superior_realsequence seq) . n) - s) by A6, XREAL_1:10;
then seq . (n + k) > ((r + ((superior_realsequence seq) . n)) - s) - ((superior_realsequence seq) . n) by XREAL_1:21;
hence ex k being Element of NAT st seq . (n + k) > r - s ; :: thesis: verum

end;

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

end;

assume A7: for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ; :: thesis: r <= lim_sup seq
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 A8: 0 < s ; :: thesis: lim_sup seq >= r - s
for n being Element of NAT holds r - s <= (superior_realsequence seq) . n

proof

let n be Element of NAT ; :: thesis: r - s <= (superior_realsequence seq) . n
consider k being Element of NAT such that
A9: r - s < seq . (n + k) by A7, A8;
seq . (n + k) <= (superior_realsequence seq) . n by A2, Th43;
hence r - s <= (superior_realsequence seq) . n by A9, XXREAL_0:2; :: thesis: verum

end;

hence lim_sup seq >= r - s by Th10; :: thesis: verum

end;

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