:: deftheorem Def2 defines Leibniz_Series_of LEIBNIZ1:def 2 :
for r being Real
for b₂ being Real_Sequence holds
( b₂ = Leibniz_Series_of r iff for n being Nat holds b₂ . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) );