for seq being ExtREAL_sequence st seq is non-increasing & -infty = inf seq holds
( seq is convergent_to_-infty & lim seq = -infty )