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