let a be positive heavy 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 )
( a <= b iff log (a,b) >= 1 ) by AG1;
hence ( a < b iff log (a,b) > 1 ) by AZ1, XXREAL_0:1; :: thesis: verum