for X being RealUnitarySpace
for x, y being Point of X holds |.(x .|. y).| <= ||.x.|| * ||.y.|| by Th19;