theorem Th9: :: MESFUNC9:9

for seq being ExtREAL_sequence
for p being ExtReal st seq is convergent & ( for k being Nat holds seq . k <= p ) holds
lim seq <= p