let z be complex number ; :: thesis: ( Im z > 0 implies sin (Arg z) > 0 )
( Re z < 0 or Re z = 0 or Re z > 0 ) ;
then A1: ( Re z < 0 or Re z > 0 or z = 0 + ((Im z) * <i> ) ) by COMPLEX1:29;
assume Im z > 0 ; :: thesis: sin (Arg z) > 0
then ( Arg z in ].(PI / 2),PI .[ or Arg z in ].0 ,(PI / 2).[ or Arg z = PI / 2 ) by A1, Th55, Th59, Th60;
then A2: ( ( PI / 2 < Arg z & Arg z < PI ) or ( 0 < Arg z & Arg z < PI / 2 ) or Arg z = PI / 2 ) by XXREAL_1:4;
then Arg z < PI by Lm2, XXREAL_0:2;
then Arg z in ].0 ,PI .[ by A2, XXREAL_1:4;
then sin . (Arg z) > 0 by Th23;
hence sin (Arg z) > 0 by SIN_COS:def 21; :: thesis: verum