let seq be Real_Sequence; :: thesis: ( seq is non-increasing implies for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
upper_bound R = seq . n )
assume A1: seq is non-increasing ; :: thesis: for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
upper_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
upper_bound R = seq . n

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

let r be Real; :: thesis: ( r in { (seq . k) where k is Nat : n <= k } implies r <= seq . n )
assume r in { (seq . k) where k is Nat : n <= k } ; :: thesis: r <= seq . n
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 r <= seq . n by A1, A3, A4, A6, SEQM_3:7; :: thesis: verum

end;

let R be Subset of REAL; :: thesis: ( R = { (seq . k) where k is Nat : n <= k } implies upper_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 } & (seq . n) - s < r )

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & (seq . n) - s < r ) )
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 } & (seq . n) - s < r )
hence ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & (seq . n) - s < r ) by A8, XREAL_1:44; :: thesis: verum

end;

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