theorem Th42: :: SPPOL_2:42

for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}