theorem th0n: :: FIELD_5:5

for n being Nat st n >= 3 holds
n + n < 2 |^ n