for e being Real
for s being Real_Sequence st s is convergent & ex k being Nat st
for i being Nat st k <= i holds
s . i <= e holds
lim s <= e by Lm3;