for a, b being Real_Sequence st ( for i being Nat holds a . i <= b . i ) & a is non-decreasing & b is non-increasing holds
( a is convergent & b is convergent )