theorem Th13: :: PRE_FF:13

for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/]