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:29;
hence sin (Arg z) <= 0 by Th53, Th54, SIN_COS:34, SIN_COS:82; :: thesis: verum