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