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,|[(q `1),(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,|[(q `1),(p `2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) )
set p1 = |[(q `1),(p `2)]|;
assume that
A1: p `1 <> q `1 and
A2: p `2 <> q `2 and
A3: f = <*p,|[(q `1),(p `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 <> |[(q `1),(p `2)]| & q <> |[(q `1),(p `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 = |[(q `1),(p `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
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,|[(q `1),(p `2)]|)) /\ (LSeg (f,2)) by A4, A7, A5, TOPREAL1:def 3
.= (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) by A4, A5, A6, TOPREAL1:def 3
.= {(f /. (i + 1))} by A5, A10, Th30 ;
:: 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 A3, A11, 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
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 ;
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 A7, A5, EUCLID:52; :: 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:52; :: thesis: verum
end;
end;