for r being Real_Sequence st ( for n being Nat holds 0 <= r . n ) holds
( ( for n being Nat holds 0 <= (Partial_Sums r) . n ) & ( for n being Nat holds r . n <= (Partial_Sums r) . n ) & ( r is summable implies ( ( for n being Nat holds (Partial_Sums r) . n <= Sum r ) & ( for n being Nat holds r . n <= Sum r ) ) ) ) by Lm1;