theorem :: HAUSDORF:36

for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds HausDist (P,P) = 0 by Th29;