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;

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 )
;

end;

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)

end;

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;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