theorem Th16: :: SERIES_1:16

for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
Partial_Sums s is non-decreasing