theorem :: HAUSDORF:41

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