for k being Nat ex N being Nat st
for x being Nat st N <= x holds
x to_power k < 2 to_power x