theorem :: NUMBER09:11

for n being Nat st n >= 2 holds
ex k being positive Nat st (2 |^ n) - 1 = (4 * k) - 1