:: deftheorem defines lim TBSP_1:def 3 :
for M being non empty MetrSpace
for S1 being sequence of M st S1 is convergent holds
for b₃ being Element of M holds
( b₃ = lim S1 iff for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S1 . m),b₃) < r );