theorem :: LIMFUNC1:60

for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) holds
abs f is divergent_in+infty_to+infty