for n being Nat
for A, B being non empty compact Subset of (TOP-REAL n) ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )