for seq being ExtREAL_sequence st seq is V116() holds
not seq is convergent_to_-infty