for n being Nat holds
( (Partial_Sums Leibniz_Series) . ((2 * n) + 1) <= Sum Leibniz_Series & Sum Leibniz_Series <= (Partial_Sums Leibniz_Series) . (2 * n) )