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