take jj ; :: thesis: not jj is zero
thus not jj is zero ; :: thesis: verum