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