let n be Nat; :: thesis: for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
(inferior_realsequence seq) . (n + 1) <= seq . n
let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies (inferior_realsequence seq) . (n + 1) <= seq . n )
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-increasing & seq is bounded_below ) ; :: thesis: (inferior_realsequence seq) . (n + 1) <= seq . n
then Y1 is bounded_below by Th32;
then A3: lower_bound Y1 <= seq . (n + 1) by A1, SEQ_4:def 2;
A4: (inferior_realsequence seq) . (n + 1) = lower_bound Y1 by Def4;
seq . (n + 1) <= seq . n by A2;
hence (inferior_realsequence seq) . (n + 1) <= seq . n by A4, A3, XXREAL_0:2; :: thesis: verum