let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. implies f is s.c.c. )
assume A1: for i, j being Nat st i + 1 < j holds
LSeg (f,i) misses LSeg (f,j) ; :: according to TOPREAL1:def 9 :: thesis: f is s.c.c.
let i be Element of NAT ; :: according to GOBOARD5:def 4 :: thesis: for b₁ being Element of NAT holds
( b₁ <= i + 1 or ( ( i <= 1 or len f <= b₁ ) & len f <= b₁ + 1 ) or LSeg (f,i) misses LSeg (f,b₁) )
let j be Element of NAT ; :: thesis: ( j <= i + 1 or ( ( i <= 1 or len f <= j ) & len f <= j + 1 ) or LSeg (f,i) misses LSeg (f,j) )
thus ( j <= i + 1 or ( ( i <= 1 or len f <= j ) & len f <= j + 1 ) or LSeg (f,i) misses LSeg (f,j) ) by A1; :: thesis: verum