let r be Real; :: thesis: ( r in [.(- 1),1.] implies Leibniz_Series_of r is summable )
set rL = Leibniz_Series_of r;
set A = abs (Leibniz_Series_of r);
set aA = alternating_series (abs (Leibniz_Series_of r));
assume r in [.(- 1),1.] ; :: thesis: Leibniz_Series_of r is summable
then ( 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 ) by Th9;
then A1: alternating_series (abs (Leibniz_Series_of r)) is summable by Th8;

per cases ( r >= 0 or r < 0 ) ;

suppose r >= 0 ; :: thesis: Leibniz_Series_of r is summable

hence Leibniz_Series_of r is summable by Th10, A1; :: thesis: verum

end;

suppose r < 0 ; :: thesis: Leibniz_Series_of r is summable

then Leibniz_Series_of r = (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) by Th10;
hence Leibniz_Series_of r is summable by A1, SERIES_1:10; :: thesis: verum

end;

end;