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