theorem Th18: :: BHSP_1:18

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