for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Nat st
for n being Nat st k <= n holds
seq . n < 0 holds
seq " is divergent_to-infty