theorem Th100: :: NUMBER08:100

for n being Nat st n > 1 holds
((3 |^ n) - (3 to_power (1 - n))) - 2 > 0