let a, b be positive Real; :: thesis: ( a > b implies log ((a / b),a) > log ((a / b),b) )
assume A1: a > b ; :: thesis: log ((a / b),a) > log ((a / b),b)
then a / b > b / b by XREAL_1:68;
then a / b > 1 by XCMPLX_1:60;
hence log ((a / b),a) > log ((a / b),b) by A1, POWER:57; :: thesis: verum