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 and
A2: not f /. 1 in Q and
A3: 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, A2, 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 A3, Th57; :: thesis: verum