for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) 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))}