let M be non empty MetrSpace; :: thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
max_dist_min (P,Q) >= 0
let P, Q be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact implies max_dist_min (P,Q) >= 0 )
assume ( P is compact & Q is compact ) ; :: thesis: max_dist_min (P,Q) >= 0
then ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) by WEIERSTR:32;
hence max_dist_min (P,Q) >= 0 by METRIC_1:5; :: thesis: verum