let a be positive light Real; :: thesis: for b being positive Real holds
( a > b iff log (a,b) > 1 )
let b be positive Real; :: thesis: ( a > b iff log (a,b) > 1 )
( 1 / a < 1 / b iff log ((1 / a),(1 / b)) > 1 ) by AG2;
hence ( a > b iff log (a,b) > 1 ) by XREAL_1:76, ABO, XREAL_1:118; :: thesis: verum