let a, b be Real; :: thesis: ( a > 1 & b > 1 implies log a,b > 0 )
assume A1: ( a > 1 & b > 1 ) ; :: thesis: log a,b > 0
then A2: a to_power (log a,b) > 1 by POWER:def 3;
assume A3: log a,b <= 0 ; :: thesis: contradiction

per cases ( log a,b = 0 or log a,b < 0 ) by A3;

suppose log a,b = 0 ; :: thesis: contradiction

hence contradiction by A2, POWER:29; :: thesis: verum

end;

suppose log a,b < 0 ; :: thesis: contradiction

hence contradiction by A1, A2, POWER:41; :: thesis: verum

end;

end;