theorem Th4: :: SERIES_1:4

for s being Real_Sequence st s is summable holds
( s is convergent & lim s = 0 )