theorem Th20: :: HAUSDORF:20

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