theorem :: BHSP_1:43

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