for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for x being set st x in P holds
(dist_min P) . x = 0