theorem Th32: :: BHSP_1:32

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