let n be 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) )
reconsider Y1 = { (seq . k) where k is Nat : n + 1 <= k } as Subset of REAL by Th29;
A1: seq . (n + 1) in Y1 ;
assume A2: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: seq . n <= (superior_realsequence seq) . (n + 1)
then Y1 is bounded_above by Th31;
then A3: seq . (n + 1) <= upper_bound Y1 by A1, SEQ_4:def 1;
A4: (superior_realsequence seq) . (n + 1) = upper_bound Y1 by Def5;
seq . n <= seq . (n + 1) by A2;
hence seq . n <= (superior_realsequence seq) . (n + 1) by A4, A3, XXREAL_0:2; :: thesis: verum