theorem :: TOPREAL3:40

for p, q being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st q <> p & (LSeg (q,p)) /\ (L~ f) = {q} holds
not p in L~ f