for seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
lim seq1 <= lim seq2