theorem Th12: :: BHSP_1:12

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