for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M holds
( (dist_min P) . x = 0 iff for r being Real st r > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < r ) )