for n being Nat
for A being non empty Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)