let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies for n being Element of NAT
for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
inf R = seq . n )
assume A1: seq is non-decreasing ; :: thesis: for n being Element of NAT
for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
inf R = seq . n
then A2: seq is bounded_below by LIMFUNC1:26;
let n be Element of NAT ; :: thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
inf R = seq . n
let R be Subset of REAL ; :: thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies inf R = seq . n )
assume A3: R = { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: inf R = seq . n
then A4: ( R <> {} & R is bounded_below ) by A2, Th32, SETLIM_1:1;
A5: for r being real number st r in R holds
seq . n <= r

proof

now

let r be real number ; :: thesis: ( r in { (seq . k) where k is Element of NAT : n <= k } implies seq . n <= r )
assume r in { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: seq . n <= r
then consider r1 being real number such that
A6: ( r = r1 & r1 in { (seq . k) where k is Element of NAT : n <= k } ) ;
consider k1 being Element of NAT such that
A7: ( r1 = seq . k1 & n <= k1 ) by A6;
consider k being Nat such that
A8: n + k = k1 by A7, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence seq . n <= r by A1, A6, A7, A8, SEQM_3:11; :: thesis: verum

end;

hence for r being real number st r in R holds
seq . n <= r by A3; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in R & r < (seq . n) + s )

proof

now

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s ) )
assume A9: 0 < s ; :: thesis: ex r being real number st
( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s )
A10: seq . n in { (seq . k) where k is Element of NAT : n <= k } ;
thus ex r being real number st
( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s ) by A9, A10, XREAL_1:31; :: thesis: verum

end;

hence for s being real number st 0 < s holds
ex r being real number st
( r in R & r < (seq . n) + s ) by A3; :: thesis: verum

end;

hence inf R = seq . n by A4, A5, SEQ_4:def 5; :: thesis: verum