let a be positive light Real; :: thesis: for c being positive heavy Real
for b, d being positive Real st log (a,b) >= log (c,d) & a < b holds
c > d
let c be positive heavy Real; :: thesis: for b, d being positive Real st log (a,b) >= log (c,d) & a < b holds
c > d
let b, d be positive Real; :: thesis: ( log (a,b) >= log (c,d) & a < b implies c > d )
assume A2: ( log (a,b) >= log (c,d) & a < b ) ; :: thesis: c > d
then log (a,b) < 1 by AM1;
then log (c,d) < 1 by A2, XXREAL_0:2;
hence c > d by AG1; :: thesis: verum