theorem :: COMSEQ_3:4

for rseq being Real_Sequence st rseq is convergent holds
for p being Real st 0 < p holds
ex n being Nat st
for m, l being Nat st n <= m & n <= l holds
|.((rseq . m) - (rseq . l)).| < p