let a, 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 AG1;
then log (c,d) >= 1 by A2, XXREAL_0:2;
hence c <= d by AG1; :: thesis: verum