let s be Real_Sequence; :: thesis: ( s is summable & ( for n being Element of NAT holds 0 <= s . n ) implies 0 <= Sum s )
assume that
A1: s is summable and
A2: for n being Element of NAT holds 0 <= s . n ; :: thesis: 0 <= Sum s
A3: Partial_Sums s is non-decreasing by A2, Th19;
A4: Partial_Sums s is convergent by A1, Def2;

now

let n be Element of NAT ; :: thesis: 0 <= (Partial_Sums s) . n
A5: (Partial_Sums s) . 0 <= (Partial_Sums s) . n by A3, SEQM_3:21;
0 <= s . 0 by A2;
hence 0 <= (Partial_Sums s) . n by A5, Def1; :: thesis: verum

end;

hence 0 <= Sum s by A4, SEQ_2:31; :: thesis: verum