let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= s . n ) implies ( Partial_Sums s is bounded_above iff s is summable ) )
assume for n being Element of NAT holds 0 <= s . n ; :: thesis: ( Partial_Sums s is bounded_above iff s is summable )
then Partial_Sums s is non-decreasing by Th19;
hence ( Partial_Sums s is bounded_above implies s is summable ) by Def2; :: thesis: ( s is summable implies Partial_Sums s is bounded_above )
assume s is summable ; :: thesis: Partial_Sums s is bounded_above
then Partial_Sums s is convergent by Def2;
then Partial_Sums s is bounded by SEQ_2:27;
hence Partial_Sums s is bounded_above ; :: thesis: verum