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

proof

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

proof

let n be Nat; :: thesis: ex k being Nat st seq . (n + k) < r + s
consider k being Nat such that
A5: seq . (n + k) < ((inferior_realsequence seq) . n) + s by A1, A4, Th40;
(inferior_realsequence seq) . n <= r by A2, A3, Th9;
then (seq . (n + k)) + ((inferior_realsequence seq) . n) < r + (((inferior_realsequence seq) . n) + s) by A5, XREAL_1:8;
then seq . (n + k) < (r + (((inferior_realsequence seq) . n) + s)) - ((inferior_realsequence seq) . n) by XREAL_1:20;
hence ex k being Nat st seq . (n + k) < r + s ; :: thesis: verum

end;

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

end;

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

proof

let s be Real; :: thesis: ( 0 < s implies lim_inf seq <= r + s )
assume A7: 0 < s ; :: thesis: lim_inf seq <= r + s
for n being Nat holds (inferior_realsequence seq) . n <= r + s

proof

let n be Nat; :: thesis: (inferior_realsequence seq) . n <= r + s
consider k being Nat such that
A8: seq . (n + k) < r + s by A6, A7;
(inferior_realsequence seq) . n <= seq . (n + k) by A1, Th40;
hence (inferior_realsequence seq) . n <= r + s by A8, 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:41; :: thesis: verum