let z be Complex; :: thesis: ( Re z > 0 implies cos (Arg z) > 0 )
( Im z < 0 or Im z = 0 or Im z > 0 ) ;
then A1: ( Im z < 0 or Im z > 0 or z = (Re z) + (0 * <i>) ) by COMPLEX1:13;
assume Re z > 0 ; :: thesis: cos (Arg z) > 0
then ( Arg z in ].0,(PI / 2).[ or Arg z in ].((3 / 2) * PI),(2 * PI).[ or Arg z = 0 ) by A1, Th35, Th41, Th44;
then cos . (Arg z) > 0 by Th15, SIN_COS:30, SIN_COS:80;
hence cos (Arg z) > 0 by SIN_COS:def 19; :: thesis: verum