:: deftheorem defines dist JORDAN1K:def 2 :
for n being Nat
for p being Point of (TOP-REAL n)
for B being Subset of (TOP-REAL n) holds dist (p,B) = dist_min ({p},B);