theorem Th14: :: FIB_NUM4:14

for n being Nat st n > 1 holds
- (1 / 2) < tau_bar to_power n