for c being Real st c > 6 holds
c ^2 < 2 to_power c by Lm9;