theorem Th11: :: BHSP_1:11

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