theorem :: BHSP_1:41

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