theorem :: JORDAN1K:44

for n being Nat
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds dist (p,A) >= 0 by Th38;