theorem Th8: :: MESFUNC9:8

for seq being ExtREAL_sequence st seq is nonnegative holds
not seq is convergent_to_-infty