let p, q be Point of (); :: thesis: for f being FinSequence of () 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 (); :: 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 ;
hence ( f /. 1 = p & f /. (len f) = q ) by ; :: thesis: f is being_S-Seq
( p <> |[(p `1),(q `2)]| & q <> |[(p `1),(q `2)]| ) by ;
hence ( f is one-to-one & len f >= 2 ) by ; :: 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 ;
A6: f /. 3 = q by ;
A7: f /. 1 = p by ;
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
A8: 1 <= i and
A9: i + 2 <= len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
i <= 1 by ;
then A10: i = 1 by ;
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (f,2)) by
.= (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) by
.= {(f /. (i + 1))} by ;
:: 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 A11: 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 ;
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
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 ;
then not not i = 0 & ... & not i = 2 ;
per cases then ( i = 1 or i = 2 ) by A12;
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 ; :: 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 ; :: thesis: verum
end;
end;