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

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