:: deftheorem defines convergent TBSP_1:def 2 :
for N being non empty MetrStruct
for S2 being sequence of N holds
( S2 is convergent iff ex x being Element of N st
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r );