let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
seq . n <= (superior_realsequence seq) . (n + 1)
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies seq . n <= (superior_realsequence seq) . (n + 1) )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: seq . n <= (superior_realsequence seq) . (n + 1)
then A2: seq . n <= seq . (n + 1) by SEQM_3:def 13;
reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29;
A3: (superior_realsequence seq) . (n + 1) = sup Y1 by Def5;
A4: ( Y1 <> {} & Y1 is bounded_above ) by A1, Th31, SETLIM_1:1;
seq . (n + 1) in Y1 ;
then seq . (n + 1) <= sup Y1 by A4, SEQ_4:def 4;
hence seq . n <= (superior_realsequence seq) . (n + 1) by A2, A3, XXREAL_0:2; :: thesis: verum