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:45;

hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; :: thesis: f is being_S-Seq

( p <> |[(p `1),(q `2)]| & q <> |[(p `1),(q `2)]| ) by A1, A2, EUCLID:52;

hence ( f is one-to-one & len f >= 2 ) by A1, A3, A4, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( f is unfolded & f is s.n.c. & f is special )

A5: f /. 2 = |[(p `1),(q `2)]| by A3, FINSEQ_4:18;

A6: f /. 3 = q by A3, FINSEQ_4:18;

A7: f /. 1 = p by A3, FINSEQ_4:18;

thus f is unfolded :: thesis: ( f is s.n.c. & f is special )

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 )

i <= 2 by A4, A13, XREAL_1:6;

then not not i = 0 & ... & not i = 2 ;

( 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:45;

hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; :: thesis: f is being_S-Seq

( p <> |[(p `1),(q `2)]| & q <> |[(p `1),(q `2)]| ) by A1, A2, EUCLID:52;

hence ( f is one-to-one & len f >= 2 ) by A1, A3, A4, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( f is unfolded & f is s.n.c. & f is special )

A5: f /. 2 = |[(p `1),(q `2)]| by A3, FINSEQ_4:18;

A6: f /. 3 = q by A3, FINSEQ_4:18;

A7: f /. 1 = p by A3, FINSEQ_4:18;

thus f is unfolded :: thesis: ( f is s.n.c. & f is special )

proof

thus
f is s.n.c.
:: thesis: f is special
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

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:6;

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 3

.= (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) by A4, A5, A6, TOPREAL1:def 3

.= {(f /. (i + 1))} by A5, A10, Th29 ;

:: thesis: verum

end;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:6;

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 3

.= (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) by A4, A5, A6, TOPREAL1:def 3

.= {(f /. (i + 1))} by A5, A10, Th29 ;

:: thesis: verum

proof

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

end;assume A11: i + 1 < j ; :: thesis: LSeg (f,i) misses LSeg (f,j)

now :: thesis: LSeg (f,i) misses LSeg (f,j)

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

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 )

i <= 2 by A4, A13, XREAL_1:6;

then not not i = 0 & ... & not i = 2 ;