theorem :: SERIES_1:27

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) & ex m being Nat st
for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 holds
not s is summable