:: deftheorem defines Cauchy BHSP_4:def 8 :
for Rseq being Real_Sequence holds
( Rseq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.((Rseq . n) - (Rseq . m)).| < r );