:: deftheorem defines HausDist HAUSDORF:def 1 :
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds HausDist (P,Q) = max ((max_dist_min (P,Q)),(max_dist_min (Q,P)));