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