:: deftheorem Def4 defines dist WEIERSTR:def 4 :
for M being non empty MetrSpace
for x being Point of M
for b₃ being Function of (TopSpaceMetr M),R^1 holds
( b₃ = dist x iff for y being Point of M holds b₃ . y = dist (y,x) );