theorem Th1: :: NAGATA_2:1

for i being Nat st i > 0 holds
ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)