theorem Th19: :: SERIES_1:19

for s1, s2 being Real_Sequence st ( for n being Nat holds 0 <= s2 . n ) & s1 is summable & ex m being Nat st
for n being Nat st m <= n holds
s2 . n <= s1 . n holds
s2 is summable