let p, q be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1 ),(q `2 )]|,q*> holds
( f /. 1 = p & f /. (len f) = q & f is being_S-Seq )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1 ),(q `2 )]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) )
set p1 = |[(p `1 ),(q `2 )]|;
assume that
A1: p `1 <> q `1 and
A2: p `2 <> q `2 and
A3: f = <*p,|[(p `1 ),(q `2 )]|,q*> ; :: thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq )
A4: len f = 1 + 2 by A3, FINSEQ_1:62;
hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:27; :: thesis: f is being_S-Seq
( p <> |[(p `1 ),(q `2 )]| & q <> |[(p `1 ),(q `2 )]| ) by A1, A2, EUCLID:56;
hence ( f is one-to-one & len f >= 2 ) by A1, A3, A4, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis: ( f is unfolded & f is s.n.c. & f is special )
A5: f /. 2 = |[(p `1 ),(q `2 )]| by A3, FINSEQ_4:27;
A6: f /. 3 = q by A3, FINSEQ_4:27;
A7: f /. 1 = p by A3, FINSEQ_4:27;
thus f is unfolded :: thesis: ( f is s.n.c. & f is special )

proof

let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} )
assume that
A8: 1 <= i and
A9: i + 2 <= len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}
i <= 1 by A4, A9, XREAL_1:8;
then A10: i = 1 by A8, XXREAL_0:1;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = (LSeg p,|[(p `1 ),(q `2 )]|) /\ (LSeg f,2) by A4, A7, A5, TOPREAL1:def 5
.= (LSeg p,|[(p `1 ),(q `2 )]|) /\ (LSeg |[(p `1 ),(q `2 )]|,q) by A4, A5, A6, TOPREAL1:def 5
.= {(f /. (i + 1))} by A5, A10, Th36 ;
:: thesis: verum

end;

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

proof

let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg f,i misses LSeg f,j )
assume A11: i + 1 < j ; :: thesis: LSeg f,i misses LSeg f,j

now

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: LSeg f,i misses LSeg f,j

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: verum

end;

suppose i <> 0 ; :: thesis: LSeg f,i misses LSeg f,j

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

end;

end;

end;

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

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
assume that
A12: 1 <= i and
A13: i + 1 <= len f ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
A14: i <= 2 by A4, A13, XREAL_1:8;
set p2 = f /. i;
set p3 = f /. (i + 1);

per cases ( i = 1 or i = 2 ) by A12, A14, NAT_1:27;

suppose i = 1 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )

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

end;

suppose i = 2 ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )

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

end;

end;