theorem Th1: :: NAT_5:1

for n being Nat holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1