let x, y, z be Element of COMPLEX ; :: thesis: ( angle x,y,z <> 0 implies angle z,y,x = (2 * PI ) - (angle x,y,z) )
assume A1: angle x,y,z <> 0 ; :: thesis: angle z,y,x = (2 * PI ) - (angle x,y,z)

now

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

case A2: (Arg (x - y)) - (Arg (z - y)) > 0 ; :: thesis: angle z,y,x = (2 * PI ) - (angle x,y,z)

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

end;

case A3: (Arg (x - y)) - (Arg (z - y)) <= 0 ; :: thesis: angle z,y,x = (2 * PI ) - (angle x,y,z)

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

end;

end;

end;

hence angle z,y,x = (2 * PI ) - (angle x,y,z) ; :: thesis: verum