for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_+infty holds
( seq2 is convergent_to_+infty & lim seq2 = +infty )