take 2 ; :: thesis: 2 is logbase
thus 2 is logbase by Def3; :: thesis: verum