let z be complex number ; :: thesis: ( z <> 0 implies ( Arg z < PI iff Arg (- z) >= PI ) )
assume A1: z <> 0 ; :: thesis: ( Arg z < PI iff Arg (- z) >= PI )
thus ( Arg z < PI implies Arg (- z) >= PI ) :: thesis: ( Arg (- z) >= PI implies Arg z < PI )

proof

assume A3: Arg z < PI ; :: thesis: Arg (- z) >= PI
Arg z >= 0 by COMPTRIG:52;
then PI + 0 <= PI + (Arg z) by XREAL_1:9;
hence Arg (- z) >= PI by A1, A3, Th22; :: thesis: verum

end;

thus ( Arg (- z) >= PI implies Arg z < PI ) :: thesis: verum

proof

assume Arg (- z) >= PI ; :: thesis: Arg z < PI
then A4: Arg (- (- z)) = (Arg (- z)) - PI by A1, Th22;
2 * PI > Arg (- z) by COMPTRIG:52;
then (PI + PI ) - PI > (Arg (- z)) - PI by XREAL_1:11;
hence Arg z < PI by A4; :: thesis: verum

end;