let x, y, z be Element of COMPLEX ; :: thesis: ( 0 <= angle x,y,z & angle x,y,z < 2 * PI )

now

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

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

Arg (x - y) >= 0 by COMPTRIG:52;
then (Arg (z - y)) + 0 <= (Arg (z - y)) + (Arg (x - y)) by XREAL_1:9;
then A2: ( Arg (z - y) < 2 * PI & (Arg (z - y)) - (Arg (x - y)) <= Arg (z - y) ) by COMPTRIG:52, XREAL_1:22;
angle x,y,z = (Arg (z - y)) - (Arg (x - y)) by A1, Def6;
hence ( 0 <= angle x,y,z & angle x,y,z < 2 * PI ) by A1, A2, XXREAL_0:2; :: thesis: verum

end;

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

Arg (z - y) >= 0 by COMPTRIG:52;
then (Arg (x - y)) + 0 <= (Arg (x - y)) + (Arg (z - y)) by XREAL_1:9;
then ( Arg (x - y) < 2 * PI & (Arg (x - y)) - (Arg (z - y)) <= Arg (x - y) ) by COMPTRIG:52, XREAL_1:22;
then (Arg (x - y)) - (Arg (z - y)) < 2 * PI by XXREAL_0:2;
then A4: (2 * PI ) - ((Arg (x - y)) - (Arg (z - y))) > 0 by XREAL_1:52;
((Arg (z - y)) - (Arg (x - y))) + (2 * PI ) < 0 + (2 * PI ) by A3, XREAL_1:10;
hence ( 0 <= angle x,y,z & angle x,y,z < 2 * PI ) by A3, A4, Def6; :: thesis: verum

end;

end;

end;

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