for f being PartFunc of REAL,REAL st f is divergent_in-infty_to+infty holds
( not f is convergent_in-infty & not f is divergent_in-infty_to-infty )