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 AG1;
hence ( a < b iff log (a,b) < 1 ) by XREAL_1:76, ABO, XREAL_1:118; :: thesis: verum