theorem :: DBLSEQ_2:30

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) )