for X being RealUnitarySpace
for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))