let x, y, z be Complex; :: thesis: angle (x,y,z) = angle ((x - y),0,(z - y))

now :: thesis: ( ( (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) >= 0 & angle ((x - y),0c,(z - y)) = angle (x,y,z) ) or ( (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) < 0 & angle ((x - y),0c,(z - y)) = angle (x,y,z) ) )

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

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

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

end;

case A2: (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) < 0 ; :: thesis: angle ((x - y),0c,(z - y)) = angle (x,y,z)

then angle ((x - y),0c,(z - y)) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by Def4;
hence angle ((x - y),0c,(z - y)) = angle (x,y,z) by A2, Def4; :: thesis: verum

end;

end;

end;

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