:: deftheorem defines absolutely_summable SERIES_1:def 4 :
for s being Real_Sequence holds
( s is absolutely_summable iff abs s is summable );