for f being FinSequence of (TOP-REAL 2) st ( for n, m being Nat st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds
LSeg (f,n) misses LSeg (f,m) ) holds
f is s.n.c.