for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
( Partial_Sums s is bounded_above iff s is summable )