theorem :: HAUSDORF:39

for n being Element of NAT
for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact holds
HausDist (P,Q) >= 0