let seq be Real_Sequence; :: thesis: ( seq is non-increasing 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
sup R = seq . n )
assume A1: seq is non-increasing ; :: 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
sup R = seq . n
then A2: seq is bounded_above 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
sup R = seq . n
let R be Subset of REAL ; :: thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies sup R = seq . n )
assume A3: R = { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: sup R = seq . n
then A4: ( R <> {} & R is bounded_above ) by A2, Th31, SETLIM_1:1;
A5: for r being real number st r in R holds
r <= seq . n

proof

now

let r be real number ; :: thesis: ( r in { (seq . k) where k is Element of NAT : n <= k } implies r <= seq . n )
assume r in { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: r <= seq . n
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 r <= seq . n by A1, A6, A7, A8, SEQM_3:13; :: thesis: verum

end;

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

end;

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

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 } & (seq . n) - s < r ) )
assume A9: 0 < s ; :: thesis: ex r being real number st
( r in { (seq . k) where k is Element of NAT : n <= k } & (seq . n) - s < r )
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 } & (seq . n) - s < r ) by A9, A10, XREAL_1:46; :: thesis: verum

end;

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

end;

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