let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. implies f is s.c.c. )
assume f is s.n.c. ; :: thesis: f is s.c.c.
then for i, j being Nat st i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) holds
LSeg (f,i) misses LSeg (f,j) by TOPREAL1:def 7;
hence f is s.c.c. by GOBOARD5:def 4; :: thesis: verum