let a, b be Real; :: thesis: ( a > 1 & b > 1 implies log (a,b) > 0 )
assume that
A1: a > 1 and
A2: b > 1 ; :: thesis: log (a,b) > 0
A3: a to_power (log (a,b)) > 1 by A1, A2, POWER:def 3;
assume A4: log (a,b) <= 0 ; :: thesis: contradiction
per cases ( log (a,b) = 0 or log (a,b) < 0 ) by A4;
suppose log (a,b) = 0 ; :: thesis: contradiction
hence contradiction by A3, POWER:24; :: thesis: verum
end;
suppose log (a,b) < 0 ; :: thesis: contradiction
hence contradiction by A1, A3, POWER:36; :: thesis: verum
end;
end;