:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
for n being Element of NAT
for P, Q being Subset of (TOP-REAL n)
for b₄ being Real holds
( b₄ = HausDist (P,Q) iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b₄ = HausDist (P9,Q9) ) );