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

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

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

then A4: |.(x + (0 * <i> )).| <> 0 by COMPLEX1:131;
A5: x + (0 * <i> ) = (|.(x + (0 * <i> )).| * (cos (Arg (x + (0 * <i> ))))) + ((|.(x + (0 * <i> )).| * (sin (Arg (x + (0 * <i> ))))) * <i> ) by A3, Def1;
then sin (Arg (x + (0 * <i> ))) = 0 by A4, COMPLEX1:163;
then ( Arg (x + (0 * <i> )) = 0 or |.(x + (0 * <i> )).| * (- 1) = x ) by A2, A5, Th33, SIN_COS:82;
then ( Arg (x + (0 * <i> )) = 0 or |.(x + (0 * <i> )).| < 0 ) by A3;
hence Arg x = 0 by COMPLEX1:132; :: thesis: verum

end;

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

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

end;

end;