for seq being ExtREAL_sequence st ( for n being Element of NAT holds seq . n <= -infty ) holds
seq is convergent_to_-infty