let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies seq is bounded )
assume ( seq is non-increasing & seq is bounded_below ) ; :: thesis: seq is bounded
then ( seq is bounded_below & seq is bounded_above ) ;
hence seq is bounded ; :: thesis: verum