let seq be Real_Sequence; :: thesis: ( seq is monotone & seq is bounded implies seq is convergent )
assume that
A1: seq is monotone and
A2: seq is bounded ; :: thesis: seq is convergent
A3: ( seq is V48() implies seq is convergent ) by A2;
( seq is V47() implies seq is convergent ) by A2;
hence seq is convergent by A1, A3, SEQM_3:def 5; :: thesis: verum