let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies inferior_realsequence seq is non-decreasing )
assume seq is bounded_below ; :: thesis: inferior_realsequence seq is non-decreasing
then for n being Element of NAT holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by Th50;
hence inferior_realsequence seq is non-decreasing by SEQM_3:def 8; :: thesis: verum