for seq, seq9, seq1 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds
seq1 is convergent