for a being Real_Sequence st a is nonnegative-yielding & a is non-increasing & a is convergent & lim a = 0 holds
( alternating_series a is summable & ( for n being Nat holds
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) ) ) )