for X being RealUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||