for X being MetrSpace
for x, y, z being Element of X holds |.((dist (x,z)) - (dist (y,z))).| <= dist (x,y)