let p, q be Point of (TOP-REAL 2); :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
set p1 = |[(p `1 ),(q `2 )]|;
assume A1: ( p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1 ),(q `2 )]|,q*> ) ; :: thesis:
then A2: ( len f = 1 + 2 & f /. 1 = p & f /. 2 = |[(p `1 ),(q `2 )]| & f /. 3 = q ) by FINSEQ_1:62, FINSEQ_4:27;
hence ( f /. 1 = p & f /. (len f) = q ) ; :: thesis:
( p <> |[(p `1 ),(q `2 )]| & q <> |[(p `1 ),(q `2 )]| ) by A1, EUCLID:56;
hence ( f is one-to-one & len f >= 2 ) by A1, A2, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis:
thus f is unfolded :: thesis:

let i be Nat; :: according to TOPREAL1:def 8 :: thesis:
assume A3: ( 1 <= i & i + 2 <= len f ) ; :: thesis:
then i <= 1 by A2, XREAL_1:8;
then A4: i = 1 by A3, XXREAL_0:1;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = (LSeg p,|[(p `1 ),(q `2 )]|) /\ (LSeg f,2) by A2, TOPREAL1:def 5
.= (LSeg p,|[(p `1 ),(q `2 )]|) /\ (LSeg |[(p `1 ),(q `2 )]|,q) by A2, TOPREAL1:def 5
.= {(f /. (i + 1))} by A2, A4, Th36 ;
:: thesis:

end;

thus f is s.n.c. :: thesis:

let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis:
assume A5: i + 1 < j ; :: thesis:

per cases ;

suppose i = 0 ; :: thesis:

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

end;

suppose i <> 0 ; :: thesis:

then LSeg f,j = {} by A1, A5, Th21;
then (LSeg f,i) /\ (LSeg f,j) = {} ;
hence LSeg f,i misses LSeg f,j by XBOOLE_0:def 7; :: thesis:

end;

hence LSeg f,i misses LSeg f,j ; :: thesis:

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis:
assume A6: ( 1 <= i & i + 1 <= len f ) ; :: thesis:
set p2 = f /. i;
set p3 = f /. (i + 1);
A7: ( i <= 2 & i > 0 ) by A2, A6, XREAL_1:8;

per cases by A7, NAT_1:27;

suppose i = 1 ; :: thesis:

hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A2, EUCLID:56; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A2, EUCLID:56; :: thesis:

end;