theorem :: JORDAN1K:49

for n being Nat
for p, q being Point of (TOP-REAL n) holds dist (p,{q}) = dist (p,q) by Th43;