let a, b be positive heavy Real; :: thesis: ( log (b,a) < 1 implies a < b )
A1: ( a > 1 & b > 1 ) by TA1;
assume B1: log (b,a) < 1 ; :: thesis: a < b
then B2: log (b,a) < log (b,b) by A1, POWER:52;
a <= b by A1, B2, POWER:57;
hence a < b by B1, AZ1, XXREAL_0:1; :: thesis: verum