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