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