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 )

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

end;

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

then A5: ((Arg (z - y)) - (Arg (x - y))) + (2 * PI ) < 0 + (2 * PI ) by XREAL_1:10;
A6: Arg (x - y) < 2 * PI by COMPTRIG:52;
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)) - (Arg (z - y)) <= Arg (x - y) by XREAL_1:22;
then (Arg (x - y)) - (Arg (z - y)) < 2 * PI by A6, XXREAL_0:2;
then (2 * PI ) - ((Arg (x - y)) - (Arg (z - y))) > 0 by XREAL_1:52;
hence ( 0 <= angle x,y,z & angle x,y,z < 2 * PI ) by A4, A5, Def6; :: thesis: verum

end;

end;

end;

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