let z be complex number ; :: thesis: ( Re z <= 0 & z <> 0 implies cos (Arg z) <= 0 )
assume that
A1: Re z <= 0 and
A2: z <> 0 ; :: thesis: cos (Arg z) <= 0
A3: 0 = 0 + (0 * <i> ) ;
( Re z < 0 or Re z = 0 ) by A1;
then ( cos (Arg z) < 0 or ( z = 0 + ((Im z) * <i> ) & ( Im z >= 0 or Im z < 0 ) ) ) by Th68, COMPLEX1:29;
then ( cos (Arg z) < 0 or ( z = 0 + ((Im z) * <i> ) & ( Im z > 0 or Im z < 0 ) ) ) by A2, A3;
hence cos (Arg z) <= 0 by Th55, Th56, SIN_COS:82; :: thesis: verum