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, Th57; :: thesis: verum