for n being Nat
for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0