theorem Th19: :: BHSP_1:19

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