theorem :: PRE_FF:14

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