theorem Th25: :: LIMFUNC1:25

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
abs seq is divergent_to+infty