for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent ;