let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) )
A1: min (((inferior_realsequence seq) . (n + 1)),(seq . n)) <= (inferior_realsequence seq) . (n + 1) by XXREAL_0:17;
assume seq is bounded_below ; :: thesis: (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
hence (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by A1, Th46; :: thesis: verum