let z be complex number ; :: thesis: ( Re z > 0 implies cos (Arg z) > 0 )
assume A1: Re z > 0 ; :: thesis: cos (Arg z) > 0
( Im z < 0 or Im z = 0 or Im z > 0 ) ;
then ( Im z < 0 or Im z > 0 or z = (Re z) + (0 * <i> ) ) by COMPLEX1:29;
then ( Arg z in ].0 ,(PI / 2).[ or Arg z in ].((3 / 2) * PI ),(2 * PI ).[ or Arg z = 0 ) by A1, Th53, Th59, Th62;
then cos . (Arg z) > 0 by Th31, SIN_COS:33, SIN_COS:85;
hence cos (Arg z) > 0 by SIN_COS:def 23; :: thesis: verum