let f be s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st n < len f holds
f | n is s.n.c.
let n be Element of NAT ; :: thesis: ( n < len f implies f | n is s.n.c. )
assume A1: n < len f ; :: 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)
A3: j in NAT by ORDINAL1:def 12;
A4: i in NAT by ORDINAL1:def 12;
A5: len (f | n) <= n by FINSEQ_5:17;

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

suppose n < j + 1 ; :: thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)

then len (f | n) < j + 1 by A5, XXREAL_0:2;
then LSeg ((f | n),j) = {} by TOPREAL1:def 3;
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 len (f | n) < j + 1 ; :: thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)

then LSeg ((f | n),j) = {} by TOPREAL1:def 3;
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 A6: j + 1 <= n and
A7: j + 1 <= len (f | n) ; :: thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)

j + 1 < len f by A1, A6, XXREAL_0:2;
then A8: LSeg (f,i) misses LSeg (f,j) by A2, A4, A3, GOBOARD5:def 4;
j <= j + 1 by NAT_1:11;
then A9: i + 1 <= j + 1 by A2, XXREAL_0:2;
LSeg (f,j) = LSeg ((f | n),j) by A7, SPPOL_2:3;
hence LSeg ((f | n),i) misses LSeg ((f | n),j) by A7, A8, A9, SPPOL_2:3, XXREAL_0:2; :: thesis: verum

end;

end;