let f be S-Sequence_in_R2; :: thesis: for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. (len f) in Q holds

(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

let Q be closed Subset of (TOP-REAL 2); :: thesis: ( L~ f meets Q & not f /. (len f) in Q implies (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )

assume that

A1: L~ f meets Q and

A2: not f /. (len f) in Q ; :: thesis: (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

set p1 = f /. 1;

set p2 = f /. (len f);

set lp = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);

A3: (L~ f) /\ Q is closed by TOPS_1:8;

len f >= 1 + 1 by TOPREAL1:def 8;

then A4: len f > 1 by NAT_1:13;

then AA: len f in dom f by FINSEQ_3:25;

L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;

then A5: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def 2;

then A6: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;

then A7: 1 <= Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;

len f in dom f by A4, FINSEQ_3:25;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . (len f) by A2, A29, PARTFUN1:def 6;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:19;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A29, XBOOLE_0:def 4;

hence (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A8, ZFMISC_1:33; :: thesis: verum

(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

let Q be closed Subset of (TOP-REAL 2); :: thesis: ( L~ f meets Q & not f /. (len f) in Q implies (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )

assume that

A1: L~ f meets Q and

A2: not f /. (len f) in Q ; :: thesis: (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

set p1 = f /. 1;

set p2 = f /. (len f);

set lp = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);

A3: (L~ f) /\ Q is closed by TOPS_1:8;

len f >= 1 + 1 by TOPREAL1:def 8;

then A4: len f > 1 by NAT_1:13;

then AA: len f in dom f by FINSEQ_3:25;

L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;

then A5: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def 2;

then A6: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;

then A7: 1 <= Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;

A8: now :: thesis: (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

A29:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q
by A5, XBOOLE_0:def 4;set m = mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f));

assume not (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} ; :: thesis: contradiction

then consider q being object such that

A9: q in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and

A10: not q in {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def 3;

reconsider q = q as Point of (TOP-REAL 2) by A9;

A11: q in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A9, XBOOLE_0:def 4;

A12: L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:42;

A13: Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;

then A14: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 <= len f by NAT_1:13;

A15: 1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = ((len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)) + 1 by A14, JORDAN4:8;

then A16: not mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)) is empty by CARD_1:27;

A17: q <> Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A10, TARSKI:def 1;

q in Q by A9, XBOOLE_0:def 4;

then A18: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A3, A11, A12, JORDAN5C:16;

end;assume not (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} ; :: thesis: contradiction

then consider q being object such that

A9: q in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and

A10: not q in {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def 3;

reconsider q = q as Point of (TOP-REAL 2) by A9;

A11: q in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A9, XBOOLE_0:def 4;

A12: L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:42;

A13: Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;

then A14: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 <= len f by NAT_1:13;

A15: 1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = ((len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)) + 1 by A14, JORDAN4:8;

then A16: not mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)) is empty by CARD_1:27;

A17: q <> Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A10, TARSKI:def 1;

q in Q by A9, XBOOLE_0:def 4;

then A18: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A3, A11, A12, JORDAN5C:16;

per cases
( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) or Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) )
;

end;

suppose
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
; :: thesis: contradiction

then A19:
q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
by A11, JORDAN3:def 3;

A21: f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;

Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A21, Th4;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A20, JORDAN5C:13;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

end;now :: thesis: not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f

then A20:
LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),q, L~ f,f /. 1,f /. (len f)
by A19, Th3, NAT_1:11;assume
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f
; :: thesis: contradiction

then (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by AA, JORDAN4:15;

hence contradiction by A19, TOPREAL1:22; :: thesis: verum

end;then (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by AA, JORDAN4:15;

hence contradiction by A19, TOPREAL1:22; :: thesis: verum

A21: f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;

Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A21, Th4;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A20, JORDAN5C:13;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

suppose A22:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
; :: thesis: contradiction

A23:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))
by A6, JORDAN3:9;

1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;

then A24: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 in dom f by A14, FINSEQ_3:25;

q in L~ (<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) by A11, A22, JORDAN3:def 3;

then A25: q in (L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) \/ (LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A16, SPPOL_2:20;

end;1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;

then A24: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 in dom f by A14, FINSEQ_3:25;

q in L~ (<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) by A11, A22, JORDAN3:def 3;

then A25: q in (L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) \/ (LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A16, SPPOL_2:20;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) or q in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1)) )
by A25, XBOOLE_0:def 3;

end;

suppose A26:
q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
; :: thesis: contradiction

f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A23, Th4;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A27, JORDAN5C:13;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

end;

now :: thesis: not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f

then A27:
LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),q, L~ f,f /. 1,f /. (len f)
by A26, Th3, NAT_1:11;assume
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f
; :: thesis: contradiction

then (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by AA, JORDAN4:15;

hence contradiction by A26, TOPREAL1:22; :: thesis: verum

end;then (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;

then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by AA, JORDAN4:15;

hence contradiction by A26, TOPREAL1:22; :: thesis: verum

f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A23, Th4;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A27, JORDAN5C:13;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

suppose A28:
q in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1))
; :: thesis: contradiction

1 in dom (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
by A16, FINSEQ_5:6;

then (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1 = (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) . 1 by PARTFUN1:def 6

.= f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A4, A14, A15, FINSEQ_6:118

.= f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A24, PARTFUN1:def 6 ;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A7, A13, A23, A28, Th4;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

end;then (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1 = (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) . 1 by PARTFUN1:def 6

.= f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A4, A14, A15, FINSEQ_6:118

.= f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A24, PARTFUN1:def 6 ;

then LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A7, A13, A23, A28, Th4;

hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

len f in dom f by A4, FINSEQ_3:25;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . (len f) by A2, A29, PARTFUN1:def 6;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:19;

then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A29, XBOOLE_0:def 4;

hence (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A8, ZFMISC_1:33; :: thesis: verum