let M be non empty MetrSpace; :: thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds

min_dist_min (P,Q) >= 0

let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies min_dist_min (P,Q) >= 0 )

assume ( P <> {} & P is compact & Q <> {} & Q is compact ) ; :: thesis: min_dist_min (P,Q) >= 0

then ex x1, x2 being Point of M st

( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) by WEIERSTR:30;

hence min_dist_min (P,Q) >= 0 by METRIC_1:5; :: thesis: verum

min_dist_min (P,Q) >= 0

let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies min_dist_min (P,Q) >= 0 )

assume ( P <> {} & P is compact & Q <> {} & Q is compact ) ; :: thesis: min_dist_min (P,Q) >= 0

then ex x1, x2 being Point of M st

( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) by WEIERSTR:30;

hence min_dist_min (P,Q) >= 0 by METRIC_1:5; :: thesis: verum