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