theorem :: COMPLEX3:101

for a, b being positive non weightless Real st log (a,b) >= 1 holds
( 0 < log (b,a) & log (b,a) <= 1 )