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