theorem :: COMPLEX2:77

for x, y, z being Complex st x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) holds
(|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2