theorem Th31: :: HAUSDORF:31

for M being non empty MetrSpace
for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min (R,Q)