theorem Th43: :: JORDAN1K:43

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