let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds x .|. (- y) = - (x .|. y)
let x, y be Point of X; :: thesis: x .|. (- y) = - (x .|. y)
x .|. (- y) = (- x) .|. y by Th17;
hence x .|. (- y) = - (x .|. y) by Th18; :: thesis: verum