for r being Real st r in [.(- 1),1.] holds
Leibniz_Series_of r is summable