theorem :: HAUSDORF:21

for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact holds
ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) )