:: deftheorem Def1 defines dist_min JORDAN1K:def 1 :
for n being Nat
for A, B being Subset of (TOP-REAL n)
for b₄ being Real holds
( b₄ = dist_min (A,B) iff ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b₄ = min_dist_min (A9,B9) ) );