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