for r being Real holds
( ( r >= 0 implies alternating_series (abs (Leibniz_Series_of r)) = Leibniz_Series_of r ) & ( r < 0 implies (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) = Leibniz_Series_of r ) )