let x be Real; :: thesis: ( x >= 0 implies Arg x = 0 )
A1: ( 0 <= Arg (x + (0 * <i>)) & Arg (x + (0 * <i>)) < 2 * PI ) by Th34;
assume A2: x >= 0 ; :: thesis: Arg x = 0

per cases ( x > - 0 or x + (0 * <i>) = 0 ) by A2;

suppose A3: x > - 0 ; :: thesis: Arg x = 0

then A4: x + (0 * <i>) = (|.(x + (0 * <i>)).| * (cos (Arg (x + (0 * <i>))))) + ((|.(x + (0 * <i>)).| * (sin (Arg (x + (0 * <i>))))) * <i>) by Def1;
|.(x + (0 * <i>)).| <> 0 by A3, COMPLEX1:45;
then sin (Arg (x + (0 * <i>))) = 0 by A4, COMPLEX1:77;
then ( Arg (x + (0 * <i>)) = 0 or |.(x + (0 * <i>)).| * (- 1) = x ) by A1, A4, Th17, SIN_COS:77;
then ( Arg (x + (0 * <i>)) = 0 or |.(x + (0 * <i>)).| < 0 ) by A3;
hence Arg x = 0 by COMPLEX1:46; :: thesis: verum

end;

suppose x + (0 * <i>) = 0 ; :: thesis: Arg x = 0

hence Arg x = 0 by Def1; :: thesis: verum

end;

end;