let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is non-decreasing holds
seq . n <= (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies seq . n <= (inferior_realsequence seq) . (n + 1) )
reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29;
A1: (inferior_realsequence seq) . (n + 1) = lower_bound Y1 by Def4;
assume A2: seq is non-decreasing ; :: thesis: seq . n <= (inferior_realsequence seq) . (n + 1)
then lower_bound Y1 = seq . (n + 1) by Th34;
hence seq . n <= (inferior_realsequence seq) . (n + 1) by A2, A1, SEQM_3:def 13; :: thesis: verum