let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r 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 ( lim_inf seq <= r 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 = inferior_realsequence seq;
assume A1: seq is bounded ; :: thesis: ( lim_inf seq <= r 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 ) ;
inferior_realsequence seq is bounded by A1, Th58;
then A3: ( inferior_realsequence seq is bounded_below & inferior_realsequence seq is bounded_above ) ;
thus ( lim_inf seq <= r 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 lim_inf seq <= r )

proof

assume A4: lim_inf seq <= r ; :: 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) < ((inferior_realsequence seq) . n) + s by A2, A5, Th42;
(inferior_realsequence seq) . n <= r by A3, A4, Th9;
then (seq . (n + k)) + ((inferior_realsequence seq) . n) < r + (((inferior_realsequence seq) . n) + s) by A6, XREAL_1:10;
then seq . (n + k) < (r + (((inferior_realsequence seq) . n) + s)) - ((inferior_realsequence seq) . n) by XREAL_1:22;
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: lim_inf seq <= r
for s being real number st 0 < s holds
lim_inf seq <= r + s

proof

let s be real number ; :: thesis: ( 0 < s implies lim_inf seq <= r + s )
assume A8: 0 < s ; :: thesis: lim_inf seq <= r + s
for n being Element of NAT holds (inferior_realsequence seq) . n <= r + s

proof

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

end;

hence lim_inf seq <= r + s by Th9; :: thesis: verum

end;

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