theorem :: BHSP_1:7

for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)