let n be Element of 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 )
assume A1: ( seq is non-increasing & seq is bounded_below ) ; :: thesis: (inferior_realsequence seq) . (n + 1) <= seq . n
then A2: seq . (n + 1) <= seq . n by SEQM_3:def 14;
reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29;
A3: (inferior_realsequence seq) . (n + 1) = inf Y1 by Def4;
A4: ( Y1 <> {} & Y1 is bounded_below ) by A1, Th32, SETLIM_1:1;
seq . (n + 1) in Y1 ;
then inf Y1 <= seq . (n + 1) by A4, SEQ_4:def 5;
hence (inferior_realsequence seq) . (n + 1) <= seq . n by A2, A3, XXREAL_0:2; :: thesis: verum