theorem Th30: :: CSSPACE:35

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