:: deftheorem Def2 defines summable SERIES_1:def 2 :
for s being Real_Sequence holds
( s is summable iff Partial_Sums s is convergent );