theorem :: SERIES_1:36

for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) & s is summable holds
s is absolutely_summable