theorem Th28: :: HAUSDORF:28

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