theorem :: TOPREAL3:39

for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st len f >= 2 & not p in L~ f holds
for n being Nat st 1 <= n & n <= len f holds
f /. n <> p