theorem :: HAUSDORF:40

for n being Element of NAT
for P being non empty Subset of (TOP-REAL n) holds HausDist (P,P) = 0