theorem :: BHSP_1:40

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))