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