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