for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0