let f be S-Sequence_in_R2; :: thesis: for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in rng f holds
(L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_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 /. 1 in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in rng f implies (L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )
assume that
A1: ( L~ f meets Q & not f /. 1 in Q ) and
A2: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in rng f ; :: thesis: (L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
(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 A1, SPRECT_4:1;
hence (L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A2, Th49; :: thesis: verum