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 /. 1 in Q ; :: thesis:
set p1 = f /. 1;
set p2 = f /. (len f);
set fp = First_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: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q by A1, A4, JORDAN5C:def 1;
then A6: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in Q by XBOOLE_0:def 4;
A7: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in L~ f by A5, XBOOLE_0:def 4;
then A8: ( 1 <= Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f & Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f <= len f ) by JORDAN3:41;
then A9: Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f in dom f by FINSEQ_3:27;
1 in dom f by A3, FINSEQ_3:27;
then First_Point (L~ f),(f /. 1),(f /. (len f)),Q <> f . 1 by A2, A6, PARTFUN1:def 8;
then First_Point (L~ f),(f /. 1),(f /. (len f)),Q in L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)) by A7, JORDAN5B:23;
then A10: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in (L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q))) /\ Q by A6, XBOOLE_0:def 4;

assume not (L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q))) /\ Q c= {(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)} ; :: thesis:
then consider q being set such that
A11: q in (L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q))) /\ Q and
A12: not q in {(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)} by TARSKI:def 3;
reconsider q = q as Point of (TOP-REAL 2) by A11;
A13: q <> First_Point (L~ f),(f /. 1),(f /. (len f)),Q by A12, TARSKI:def 1;
A14: q in Q by A11, XBOOLE_0:def 4;
A15: q in L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)) by A11, XBOOLE_0:def 4;
L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)) c= L~ f by A7, JORDAN3:76;
then A16: LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f) by A4, A14, A15, JORDAN5C:15;

per cases ;

suppose First_Point (L~ f),(f /. 1),(f /. (len f)),Q = f . 1 ; :: thesis:

then A17: q in L~ <*(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)*> by A15, JORDAN3:def 5;
len <*(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)*> = 1 by FINSEQ_1:56;
hence contradiction by A17, TOPREAL1:28; :: thesis:

end;

suppose A18: First_Point (L~ f),(f /. 1),(f /. (len f)),Q <> f . 1 ; :: thesis:

set m = mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f);
len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) = ((Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) -' 1) + 1 by A8, JORDAN4:20;
then len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) <> 0 by NAT_1:11;
then A19: not mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) is empty by CARD_1:47;
q in L~ ((mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) ^ <*(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)*>) by A15, A18, JORDAN3:def 5;
then A20: q in (L~ (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f))) \/ (LSeg ((mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) /. (len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)))),(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)) by A19, SPPOL_2:19;
A21: Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f < len f by A7, JORDAN3:41;
A22: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) by A7, JORDAN3:42;

per cases by A20, XBOOLE_0:def 3;

suppose A23: q in L~ (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) ; :: thesis:

A24: now

assume Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f <= 1 ; :: thesis:
then Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f = 1 by A8, XXREAL_0:1;
then len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) = 1 by A3, JORDAN4:27;
hence contradiction by A23, TOPREAL1:28; :: thesis:

end;

then A25: LE q,f /. (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f), L~ f,f /. 1,f /. (len f) by A8, A23, SPRECT_3:33;
f /. (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) in LSeg (f /. (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)),(First_Point (L~ f),(f /. 1),(f /. (len f)),Q) by RLTOPSP1:69;
then LE f /. (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f), First_Point (L~ f),(f /. 1),(f /. (len f)),Q, L~ f,f /. 1,f /. (len f) by A21, A22, A24, SPRECT_3:40;
then LE q, First_Point (L~ f),(f /. 1),(f /. (len f)),Q, L~ f,f /. 1,f /. (len f) by A25, JORDAN5C:13;
hence contradiction by A13, A16, JORDAN5C:12, TOPREAL1:31; :: thesis:

end;

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

len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) in dom (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) by A19, FINSEQ_5:6;
then (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) /. (len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f))) = (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f)) . (len (mid f,1,(Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f))) by PARTFUN1:def 8
.= f . (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) by A8, JORDAN4:22
.= f /. (Index (First_Point (L~ f),(f /. 1),(f /. (len f)),Q),f) by A9, PARTFUN1:def 8 ;
then LE q, First_Point (L~ f),(f /. 1),(f /. (len f)),Q, L~ f,f /. 1,f /. (len f) by A8, A21, A22, A26, SPRECT_3:40;
hence contradiction by A13, A16, JORDAN5C:12, TOPREAL1:31; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence (L~ (R_Cut f,(First_Point (L~ f),(f /. 1),(f /. (len f)),Q))) /\ Q = {(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)} by A10, ZFMISC_1:39; :: thesis: