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