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 consider x1, x2 being Point of M such that
A1: ( x1 in P & x2 in Q & dist x1,x2 = min_dist_min P,Q ) by WEIERSTR:36;
thus min_dist_min P,Q >= 0 by A1, METRIC_1:5; :: thesis: verum