let f be S-Sequence_in_R2; :: thesis:
let Q be closed Subset of (TOP-REAL 2); :: thesis:
assume that
A1: L~ f meets Q and
A2: not f /. (len f) in Q ; :: thesis:
set p1 = f /. 1;
set p2 = f /. (len f);
set lp = Last_Point (L~ f),(f /. 1),(f /. (len f)),Q;
len f >= 1 + 1 by TOPREAL1:def 10;
then A3: len f > 1 by NAT_1:13;
A4: (L~ f) /\ Q is closed by TOPS_1:35;
L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:31;
then A5: Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q by A1, A4, JORDAN5C:def 2;
then A6: Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in Q by XBOOLE_0:def 4;
A7: Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in L~ f by A5, XBOOLE_0:def 4;
then A8: ( 1 <= Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f & Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f <= len f ) by JORDAN3:41;
len f in dom f by A3, FINSEQ_3:27;
then Last_Point (L~ f),(f /. 1),(f /. (len f)),Q <> f . (len f) by A2, A6, PARTFUN1:def 8;
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 A7, JORDAN5B:22;
then A9: 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 A6, XBOOLE_0:def 4;

now

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:
then consider q being set such that
A10: q in (L~ (L_Cut f,(Last_Point (L~ f),(f /. 1),(f /. (len f)),Q))) /\ Q and
A11: 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 A10;
A12: q <> Last_Point (L~ f),(f /. 1),(f /. (len f)),Q by A11, TARSKI:def 1;
A13: q in Q by A10, XBOOLE_0:def 4;
A14: q in L~ (L_Cut f,(Last_Point (L~ f),(f /. 1),(f /. (len f)),Q)) by A10, XBOOLE_0:def 4;
L~ (L_Cut f,(Last_Point (L~ f),(f /. 1),(f /. (len f)),Q)) c= L~ f by A7, JORDAN3:77;
then A15: LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q, L~ f,f /. 1,f /. (len f) by A4, A13, A14, JORDAN5C:16;
set m = mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f);
A16: Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f < len f by A7, JORDAN3:41;
then A17: (Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1 <= len f by NAT_1:13;
A18: 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 A17, JORDAN4:20;
then len (mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f)) <> 0 by NAT_1:11;
then A19: not mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f) is empty by CARD_1:47;

per cases ;

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:

then A20: q in L~ (mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f)) by A14, JORDAN3:def 4;
A21: 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 A7, JORDAN3:42;

now

assume (Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1 >= len f ; :: thesis:
then (Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1 = len f by A17, XXREAL_0:1;
then len (mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f)) = 1 by A3, JORDAN4:27;
hence contradiction by A20, TOPREAL1:28; :: thesis:

end;

then A22: LE f /. ((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),q, L~ f,f /. 1,f /. (len f) by A20, Th4, NAT_1:11;
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:69;
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 A8, A16, A21, Th5;
then LE Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f) by A22, JORDAN5C:13;
hence contradiction by A12, A15, JORDAN5C:12, TOPREAL1:31; :: thesis:

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:

then 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 A14, JORDAN3:def 4;
then A23: 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 A19, SPPOL_2:20;
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 A17, FINSEQ_3:27;
A25: 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 A7, JORDAN3:42;

now

per cases by A23, XBOOLE_0:def 3;

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

now

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 A26, Th4, NAT_1:11;
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:69;
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 A8, A16, A25, Th5;
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 A12, A15, JORDAN5C:12, TOPREAL1:31; :: thesis:

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:

1 in dom (mid f,((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1),(len f)) by A19, 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 8
.= f . ((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1) by A3, A17, A18, JORDAN3:27
.= f /. ((Index (Last_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) + 1) by A24, PARTFUN1:def 8 ;
then LE Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f) by A8, A16, A25, A28, Th5;
hence contradiction by A12, A15, JORDAN5C:12, TOPREAL1:31; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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 A9, ZFMISC_1:39; :: thesis: