let f be FinSequence of (TOP-REAL 2); :: thesis: ( ( for n, m being Element of 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 Element of 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 9 :: 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:27;
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 5;
hence LSeg f,n misses LSeg f,m by XBOOLE_1:65; :: thesis: verum

end;

end;