let x, y, z be Element of COMPLEX ; :: thesis: angle x,y,z = angle (x - y),0 ,(z - y)

now

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 Def6;
hence angle (x - y),0c ,(z - y) = angle x,y,z by A1, Def6; :: 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 Def6;
hence angle (x - y),0c ,(z - y) = angle x,y,z by A2, Def6; :: thesis: verum

end;

end;

end;

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