take 1 --> (- jj) ; :: thesis: ( 1 --> (- jj) is negative-yielding & 1 --> (- jj) is real-valued )
thus ( 1 --> (- jj) is negative-yielding & 1 --> (- jj) is real-valued ) ; :: thesis: verum