:: deftheorem defines Leibniz_Series LEIBNIZ1:def 3 :
Leibniz_Series = Leibniz_Series_of 1;