let x, y, z be Complex; ( x <> y & z <> y implies ( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) ) )
assume
( x <> y & z <> y )
; ( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) )
then A1:
( x - y <> 0c & z - y <> 0c )
;
angle (x,y,z) = angle ((x - y),0c,(z - y))
by Th69;
hence
( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) )
by A1, Th73; verum