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 `1)) / 2),(p `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 `1)) / 2),(p `2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) )
set p1 = |[(((p `1) + (q `1)) / 2),(p `2)]|;
assume that
A1: p `1 <> q `1 and
A2: p `2 = q `2 and
A3: f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ; :: thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq )
A4: |[(((p `1) + (q `1)) / 2),(p `2)]| `1 = ((p `1) + (q `1)) / 2 ;
A5: len f = 1 + 2 by A3, FINSEQ_1:45;
hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; :: thesis: f is being_S-Seq
( p `1 <> ((p `1) + (q `1)) / 2 & q `1 <> ((p `1) + (q `1)) / 2 ) by A1;
hence ( f is one-to-one & len f >= 2 ) by A1, A3, A5, A4, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( f is unfolded & f is s.n.c. & f is special )
A6: f /. 2 = |[(((p `1) + (q `1)) / 2),(p `2)]| by A3, FINSEQ_4:18;
A7: f /. 3 = q by A3, FINSEQ_4:18;
A8: f /. 1 = p by A3, FINSEQ_4:18;
thus f is unfolded :: thesis: ( f is s.n.c. & f is special )

proof

let i be Nat; :: according to TOPREAL1:def 6 :: 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:6;
then A11: i = 1 by A9, XXREAL_0:1;
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (f,2)) by A5, A8, A6, TOPREAL1:def 3
.= (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) by A5, A6, A7, TOPREAL1:def 3
.= {(f /. (i + 1))} by A1, A2, A6, A11, Th32 ;
:: thesis: verum

end;

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

proof

let i, j be Nat; :: according to TOPREAL1:def 7 :: 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 :: thesis: LSeg (f,i) misses LSeg (f,j)

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 3;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ;
hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum

end;

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

then LSeg (f,j) = {} by A3, A12, Th15;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ;
hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum

end;

end;

end;

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

end;

let i be Nat; :: according to TOPREAL1:def 5 :: 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 )
i <= 2 by A5, A14, XREAL_1:6;
then not not i = 0 & ... & not i = 2 ;

per cases then ( i = 1 or i = 2 ) by A13;

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; :: 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 A2, A6, A7; :: thesis: verum

end;

end;