theorem Th3: :: LOPBAN_3:3

for X being RealNormSpace
for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||