let f be FinSequence of (TOP-REAL 2); :: thesis: ( ( 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) ) implies f is s.n.c. )
assume A1: 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) ; :: thesis: f is s.n.c.
let n, m be Nat; :: according to TOPREAL1:def 7 :: thesis: ( m <= n + 1 or LSeg (f,n) misses LSeg (f,m) )
assume A2: m > n + 1 ; :: thesis: LSeg (f,n) misses LSeg (f,m)
A3: ( n <= n + 1 & m <= m + 1 ) by NAT_1:11;

per cases ( ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) or not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ;

suppose ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) ; :: thesis: LSeg (f,n) misses LSeg (f,m)

hence LSeg (f,n) misses LSeg (f,m) by A1, A2; :: thesis: verum

end;

suppose ( not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ; :: thesis: LSeg (f,n) misses LSeg (f,m)

then ( not 1 <= n or not n <= len f or not 1 <= n + 1 or not n + 1 <= len f or not 1 <= m or not m <= len f or not 1 <= m + 1 or not m + 1 <= len f ) by FINSEQ_3:25;
then ( not 1 <= n or not n + 1 <= len f or not 1 <= m or not m + 1 <= len f ) by A3, XXREAL_0:2;
then ( LSeg (f,m) = {} or LSeg (f,n) = {} ) by TOPREAL1:def 3;
hence LSeg (f,n) misses LSeg (f,m) ; :: thesis: verum

end;

end;