theorem Th16: :: SEQ_2:16

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|