let X be RealUnitarySpace; :: 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 Th8
.= - (- (x .|. y)) by Th8 ;
hence (- x) .|. (- y) = x .|. y ; :: thesis: verum