let x, y, z be Complex; :: thesis: ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI )
now :: thesis: ( ( (Arg (z - y)) - (Arg (x - y)) >= 0 & 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) or ( (Arg (z - y)) - (Arg (x - y)) < 0 & 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) )
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:34;
then (Arg (z - y)) + 0 <= (Arg (z - y)) + (Arg (x - y)) by XREAL_1:7;
then A2: ( Arg (z - y) < 2 * PI & (Arg (z - y)) - (Arg (x - y)) <= Arg (z - y) ) by COMPTRIG:34, XREAL_1:20;
angle (x,y,z) = (Arg (z - y)) - (Arg (x - y)) by A1, Def4;
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:34;
then (Arg (x - y)) + 0 <= (Arg (x - y)) + (Arg (z - y)) by XREAL_1:7;
then ( Arg (x - y) < 2 * PI & (Arg (x - y)) - (Arg (z - y)) <= Arg (x - y) ) by COMPTRIG:34, XREAL_1:20;
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:50;
((Arg (z - y)) - (Arg (x - y))) + (2 * PI) < 0 + (2 * PI) by A3, XREAL_1:8;
hence ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) by A3, A4, Def4; :: thesis: verum
end;
end;
end;
hence ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) ; :: thesis: verum