theorem Th23: :: HAUSDORF:23

for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact & Q is compact & z in Q holds
(dist_max P) . z <= max_dist_max (P,Q)