let z be Complex; :: thesis: ( Im z <= 0 implies sin (Arg z) <= 0 )
assume Im z <= 0 ; :: thesis: sin (Arg z) <= 0
then ( Im z < 0 or Im z = 0 ) ;
then ( sin (Arg z) < 0 or ( z = (Re z) + (0 * <i>) & ( Re z >= 0 or Re z < 0 ) ) ) by Th46, COMPLEX1:13;
hence sin (Arg z) <= 0 by Th35, Th36, SIN_COS:31, SIN_COS:77; :: thesis: verum