for seq, seq1 being Real_Sequence st seq is divergent_to-infty & ( for n being Nat holds seq1 . n <= seq . n ) holds
seq1 is divergent_to-infty