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 ),(((p `2 ) + (q `2 )) / 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 ),(((p `2 ) + (q `2 )) / 2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) )
set p1 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|;
assume that
A1: p `1 = q `1 and
A2: p `2 <> q `2 and
A3: f = <*p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q*> ; :: thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq )
A4: |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `2 = ((p `2 ) + (q `2 )) / 2 by EUCLID:56;
A5: 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 `2 <> ((p `2 ) + (q `2 )) / 2 & q `2 <> ((p `2 ) + (q `2 )) / 2 ) by A2;
hence ( f is one-to-one & len f >= 2 ) by A2, A3, A5, A4, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis: ( f is unfolded & f is s.n.c. & f is special )
A6: f /. 2 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A3, FINSEQ_4:27;
A7: f /. 3 = q by A3, FINSEQ_4:27;
A8: 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
A9: 1 <= i and
A10: i + 2 <= len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}
i <= 1 by A5, A10, XREAL_1:8;
then A11: i = 1 by A9, XXREAL_0:1;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = (LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|) /\ (LSeg f,2) by A5, A8, A6, TOPREAL1:def 5
.= (LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|) /\ (LSeg |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q) by A5, A6, A7, TOPREAL1:def 5
.= {(f /. (i + 1))} by A1, A2, A6, A11, Th38 ;
:: 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 A12: 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, A12, 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
A13: 1 <= i and
A14: i + 1 <= len f ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
A15: i <= 2 by A5, A14, XREAL_1:8;
set p2 = f /. i;
set p3 = f /. (i + 1);

per cases ( i = 1 or i = 2 ) by A13, A15, 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 A8, A6, 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 A1, A6, A7, EUCLID:56; :: thesis: verum

end;

end;