for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds
for n being Nat holds seq . n < 0