let n be Nat; :: thesis: for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0
let A, B be non empty Subset of (TOP-REAL n); :: thesis: dist_min (A,B) >= 0
ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1;
hence dist_min (A,B) >= 0 by Th11; :: thesis: verum