let x, y, z be Element of COMPLEX ; :: thesis: ( angle x,y,z = 0 implies ( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 ) )
assume A1: angle x,y,z = 0 ; :: thesis: ( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 )

now

per cases ( (Arg (z - y)) - (Arg (x - y)) >= 0 or (Arg (z - y)) - (Arg (x - y)) < 0 ) ;

case (Arg (z - y)) - (Arg (x - y)) >= 0 ; :: thesis: ( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 )

then (Arg (z - y)) - (Arg (x - y)) = 0 by A1, Def6;
hence ( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 ) by Def6; :: thesis: verum

end;

case A2: (Arg (z - y)) - (Arg (x - y)) < 0 ; :: thesis: contradiction

then - ((Arg (z - y)) - (Arg (x - y))) > 0 ;
then A3: angle z,y,x = (Arg (x - y)) - (Arg (z - y)) by Def6;
angle x,y,z = (2 * PI ) + ((Arg (z - y)) - (Arg (x - y))) by A2, Def6;
hence contradiction by A1, A3, Th84; :: thesis: verum

end;

end;

end;

hence ( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 ) ; :: thesis: verum