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