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