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