for seq being ExtREAL_sequence st seq is convergent_to_+infty holds
( not seq is convergent_to_-infty & not seq is convergent_to_finite_number )