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 = ((- 1) * x) .|. y by RLVECT_1:16
.= (- 1) * (x .|. y) by Def2
.= x .|. ((- 1) * y) by Def2 ;
hence (- x) .|. y = x .|. (- y) by RLVECT_1:16; :: thesis: verum