take X --> (- jj) ; :: thesis: X --> (- jj) is negative-yielding
thus X --> (- jj) is negative-yielding ; :: thesis: verum