let x, y, z be 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 :: thesis: ( ( (Arg (z - y)) - (Arg (x - y)) >= 0 & Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) or ( (Arg (z - y)) - (Arg (x - y)) < 0 & contradiction ) )

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, Def4;
hence ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) by Def4; :: 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 Def4;
angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by A2, Def4;
hence contradiction by A1, A3, Th68; :: thesis: verum

end;

end;

end;

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