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