:: deftheorem Def9 defines lim TOPRNS_1:def 9 :
for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
for b₃ being Point of (TOP-REAL N) holds
( b₃ = lim seq iff for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₃).| < r );