let f be S-Sequence_in_R2; :: thesis: for Q being closed Subset of () 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 (); :: 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 ;
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))}
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 () by A9;
A11: q in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by ;
A12: L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by ;
A13: Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by ;
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 ;
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 ;
q in Q by ;
then A18: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by ;
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) ) ;
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 ;
now :: thesis: not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f
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 ;
then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by ;
hence contradiction by A19, TOPREAL1:22; :: thesis: verum
end;
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 ;
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 ;
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 ;
hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum
end;
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 ;
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 ;
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 ;
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 ;
per 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 ;
suppose A26: q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) ; :: thesis: contradiction
now :: thesis: not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f
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 ;
then len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by ;
hence contradiction by A26, TOPREAL1:22; :: thesis: verum
end;
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 ;
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 ;
hence contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; :: thesis: verum
end;
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 ;
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
.= f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by ;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
A29: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q by ;
len f in dom f by ;
then Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . (len f) by ;
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 ;
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 ;
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 ; :: thesis: verum