take jj ; :: thesis: jj is positive
thus jj is positive ; :: thesis: verum