theorem Th8: :: BHSP_1:8

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