let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st f is s.n.c. holds
f | n is s.n.c.
let n be 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 7 :: 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 :: thesis: ( ( i = 0 & LSeg ((f | n),i) = {} ) or ( j + 1 > len (f | n) & LSeg ((f | n),j) = {} ) )

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 3; :: thesis: verum

end;

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

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

end;

end;

end;

then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = {} ;
hence LSeg ((f | n),i) misses LSeg ((f | n),j) ; :: 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;
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
.= {} by A5, A4, Th3 ;
hence LSeg ((f | n),i) misses LSeg ((f | n),j) ; :: thesis: verum

end;

end;