theorem Th11: :: LEIBNIZ1:11
for r being Real st r in [.(- 1),1.] holds
Leibniz_Series_of r is summable