let x, y, z be Element of 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 A1: ( 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 A2: x - y <> 0c ;
A3: z - y <> 0c by A1;
angle x,y,z = angle (x - y),0c ,(z - y) by Th85;
hence ( Re ((x - y) .|. (z - y)) = 0 iff ( angle x,y,z = PI / 2 or angle x,y,z = (3 / 2) * PI ) ) by A2, A3, Th89; :: thesis: verum