theorem :: LIMFUNC2:24

for x0 being Real
for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds
abs f is_right_divergent_to+infty_in x0