for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )