let f be S-Sequence_in_R2; :: thesis: for Q being closed Subset of () st L~ f meets Q & not f /. 1 in Q holds
(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))}

let Q be closed Subset of (); :: thesis: ( L~ f meets Q & not f /. 1 in Q implies (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))} )
assume that
A1: L~ f meets Q and
A2: not f /. 1 in Q ; :: thesis: (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))}
set p1 = f /. 1;
set p2 = f /. (len f);
set fp = First_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: 1 in dom f by FINSEQ_3:25;
L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;
then A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by ;
then A6: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;
then A7: 1 <= Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;
A8: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= len f by ;
then A9: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) in dom f by ;
A10: now :: thesis: (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))}
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: contradiction
then consider q being object 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 () by A11;
A13: q in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by ;
A14: L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by ;
A15: q <> First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by ;
q in Q by ;
then A16: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by ;
per cases ( First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1 or First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 ) ;
suppose A17: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1 ; :: thesis: contradiction
A18: len <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> = 1 by FINSEQ_1:39;
q in L~ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> by ;
hence contradiction by A18, TOPREAL1:22; :: thesis: verum
end;
suppose A19: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 ; :: thesis: contradiction
set m = mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)));
A20: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by ;
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 ;
then A21: not mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) is empty by CARD_1:27;
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 ;
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 ;
then A23: 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 ;
per cases ( q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) or 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))) ) by ;
suppose A24: q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) ; :: thesis: contradiction
A25: now :: thesis: not Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= 1
assume Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= 1 ; :: thesis: contradiction
then Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) = 1 by ;
then len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = 1 by ;
hence contradiction by A24, TOPREAL1:22; :: thesis: verum
end;
then A26: LE q,f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), L~ f,f /. 1,f /. (len f) by ;
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:68;
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 ;
then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by ;
hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum
end;
suppose A27: 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: contradiction
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 ;
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 6
.= f . (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by
.= f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by ;
then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by ;
hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
A28: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q by ;
1 in dom f by ;
then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 by ;
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 ;
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))))) /\ Q by ;
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 ; :: thesis: verum