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
((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds
not s is summable