let f be S-Sequence_in_R2; 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); ( 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
; (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; verum