theorem Th32: :: HAUSDORF:32

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 <= HausDist (Q,R)