:: deftheorem Def5 defines dist_max WEIERSTR:def 5 :
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for b₃ being Function of (TopSpaceMetr M),R^1 holds
( b₃ = dist_max P iff for x being Point of M holds b₃ . x = upper_bound ((dist x) .: P) );