theorem Th30: :: BHSP_1:30

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