let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
set seq1 = inferior_realsequence seq;
assume A1: seq is bounded ; :: thesis: ( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
then A2: ( seq is bounded_below & seq is bounded_above ) ;
inferior_realsequence seq is bounded by A1, Th58;
then A3: ( inferior_realsequence seq is bounded_below & inferior_realsequence seq is bounded_above ) ;
thus ( r <= lim_inf seq implies for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) :: thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) implies r <= lim_inf seq )

proof

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

proof

consider n1 being Element of NAT such that
A6: (inferior_realsequence seq) . n1 > (sup (inferior_realsequence seq)) - s by A3, A5, Th7;
((inferior_realsequence seq) . n1) + (sup (inferior_realsequence seq)) > r + ((sup (inferior_realsequence seq)) - s) by A4, A6, XREAL_1:10;
then ((inferior_realsequence seq) . n1) + (sup (inferior_realsequence seq)) > (r - s) + (sup (inferior_realsequence seq)) ;
then A7: (((inferior_realsequence seq) . n1) + (sup (inferior_realsequence seq))) - (sup (inferior_realsequence seq)) > r - s by XREAL_1:22;

now

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

end;

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

end;

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

proof

let s be real number ; :: thesis: ( 0 < s implies r - s <= lim_inf seq )
assume A9: 0 < s ; :: thesis: r - s <= lim_inf seq
consider n1 being Element of NAT such that
A10: for k being Element of NAT holds r - s < seq . (n1 + k) by A8, A9;
for k being Element of NAT holds r - s <= seq . (n1 + k) by A10;
then A11: r - s <= (inferior_realsequence seq) . n1 by A2, Th44;
(inferior_realsequence seq) . n1 <= sup (inferior_realsequence seq) by A3, Th7;
hence r - s <= lim_inf seq by A11, XXREAL_0:2; :: thesis: verum

end;

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