theorem Th9: :: LEIBNIZ1:9

for r being Real st r in [.(- 1),1.] holds
( abs (Leibniz_Series_of r) is nonnegative-yielding & abs (Leibniz_Series_of r) is non-increasing & abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 )