take 1 ; :: thesis: not 1 is logbase
thus not 1 is logbase by Def3; :: thesis: verum