let x, y, z be Complex; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum