let a, b be Real; :: thesis: ( 1 < a & 1 < b implies 0 < log (a,b) )
assume that
A1: 1 < a and
A2: 1 < b ; :: thesis: 0 < log (a,b)
log (a,1) = 0 by A1, POWER:51;
hence 0 < log (a,b) by A1, A2, POWER:57; :: thesis: verum