let z be complex number ; :: 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 Th64, COMPLEX1:13;
hence sin (Arg z) <= 0 by Th53, Th54, SIN_COS:31, SIN_COS:77; :: thesis: verum