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 Th18
.= - (- (x .|. y)) by Th19 ;
hence (- x) .|. (- y) = x .|. y ; :: thesis: verum