let z be Complex; :: 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 Th49, COMPLEX1:13;
hence cos (Arg z) >= 0 by Def1, Th37, Th38, SIN_COS:31, SIN_COS:77; :: thesis: verum