take X --> 1 ; :: thesis: X --> 1 is positive-yielding
thus X --> 1 is positive-yielding ; :: thesis: verum