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

per cases ( i = 0 or j + 1 > len (f | n) or ( i <> 0 & j + 1 <= len (f | n) ) ) ;

suppose A3: ( i = 0 or j + 1 > len (f | n) ) ; :: thesis: LSeg (f | n),i misses LSeg (f | n),j

now

per cases ( i = 0 or j + 1 > len (f | n) ) by A3;

case i = 0 ; :: thesis: LSeg (f | n),i = {}

hence LSeg (f | n),i = {} by TOPREAL1:def 5; :: thesis: verum

end;

case j + 1 > len (f | n) ; :: thesis: LSeg (f | n),j = {}

hence LSeg (f | n),j = {} by TOPREAL1:def 5; :: thesis: verum

end;

end;

end;

then (LSeg (f | n),i) /\ (LSeg (f | n),j) = {} ;
hence LSeg (f | n),i misses LSeg (f | n),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose that i <> 0 and
A4: j + 1 <= len (f | n) ; :: thesis: LSeg (f | n),i misses LSeg (f | n),j

A5: LSeg f,i misses LSeg f,j by A1, A2, TOPREAL1:def 9;
j <= j + 1 by NAT_1:11;
then i + 1 < j + 1 by A2, XXREAL_0:2;
then (LSeg (f | n),i) /\ (LSeg (f | n),j) = (LSeg f,i) /\ (LSeg (f | n),j) by A4, Th3, XXREAL_0:2
.= (LSeg f,i) /\ (LSeg f,j) by A4, Th3
.= {} by A5, XBOOLE_0:def 7 ;
hence LSeg (f | n),i misses LSeg (f | n),j by XBOOLE_0:def 7; :: thesis: verum

end;

end;