let a, b be positive non weightless Real; :: thesis: ( log (a,b) >= 1 implies ( 0 < log (b,a) & log (b,a) <= 1 ) )
assume A2: log (a,b) >= 1 ; :: thesis: ( 0 < log (b,a) & log (b,a) <= 1 )
(log (a,b)) / (log (a,b)) >= 1 / (log (a,b)) by A2, XREAL_1:72;
then 1 >= 1 / (log (a,b)) by A2, XCMPLX_1:60;
hence ( 0 < log (b,a) & log (b,a) <= 1 ) by A2, ABA; :: thesis: verum