:: deftheorem defines max_dist_min WEIERSTR:def 8 :
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds max_dist_min (P,Q) = upper_bound ((dist_min P) .: Q);