theorem ABA: :: COMPLEX3:92

for a, b being positive non weightless Real holds log (a,b) = 1 / (log (b,a))