let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n )
assume A1: seq is non-decreasing ; :: thesis: for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n
let n be Nat; :: thesis: for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n

A2: now :: thesis: for r being Real st r in { (seq . k) where k is Nat : n <= k } holds
seq . n <= r

let r be Real; :: thesis: ( r in { (seq . k) where k is Nat : n <= k } implies seq . n <= r )
assume r in { (seq . k) where k is Nat : n <= k } ; :: thesis: seq . n <= r
then consider r1 being Real such that
A3: ( r = r1 & r1 in { (seq . k) where k is Nat : n <= k } ) ;
consider k1 being Nat such that
A4: r1 = seq . k1 and
A5: n <= k1 by A3;
consider k being Nat such that
A6: n + k = k1 by A5, NAT_1:10;
thus seq . n <= r by A1, A3, A4, A6, SEQM_3:5; :: thesis: verum

end;

let R be Subset of REAL; :: thesis: ( R = { (seq . k) where k is Nat : n <= k } implies lower_bound R = seq . n )

A7: now :: thesis: for s being Real st 0 < s holds
ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s )

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s ) )
A8: seq . n in { (seq . k) where k is Nat : n <= k } ;
assume 0 < s ; :: thesis: ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s )
hence ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s ) by A8, XREAL_1:29; :: thesis: verum

end;

assume A9: R = { (seq . k) where k is Nat : n <= k } ; :: thesis: lower_bound R = seq . n
then A10: R <> {} by SETLIM_1:1;
R is bounded_below by A1, A9, Th32, LIMFUNC1:1;
hence lower_bound R = seq . n by A9, A10, A2, A7, SEQ_4:def 2; :: thesis: verum