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