let z be Complex; :: 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 Th50, COMPLEX1:13;
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 Th37, Th38, SIN_COS:77; :: thesis: verum