theorem :: HAUSDORF:30

for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
min_dist_max (P,Q) >= 0