let x be Real; :: thesis: ( x < 0 implies Arg x = PI )
assume A1: x < 0 ; :: thesis: Arg x = PI
A2: ( 0 <= Arg (x + (0 * <i> )) & Arg (x + (0 * <i> )) < 2 * PI ) by Th52;
A3: |.(x + (0 * <i> )).| <> 0 by A1, COMPLEX1:131;
A4: x + (0 * <i> ) = (|.(x + (0 * <i> )).| * (cos (Arg (x + (0 * <i> ))))) + ((|.(x + (0 * <i> )).| * (sin (Arg (x + (0 * <i> ))))) * <i> ) by A1, Def1;
then sin (Arg (x + (0 * <i> ))) = 0 by A3, COMPLEX1:163;
then ( Arg (x + (0 * <i> )) = PI or |.(x + (0 * <i> )).| * 1 = x ) by A2, A4, Th33, SIN_COS:34;
hence Arg x = PI by A1, COMPLEX1:132; :: thesis: verum