theorem :: JORDAN1K:45

for n being Nat
for A being compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st p in A holds
dist (p,A) = 0 by Th39, ZFMISC_1:48;