for seq being Real_Sequence st seq is summable holds
for eps being Real st eps > 0 holds
ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps