theorem Th42: :: LIMFUNC1:42

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