let c be Real; :: thesis: ( c > 6 implies c ^2 < 2 to_power c )
assume A1: c > 6 ; :: thesis: c ^2 < 2 to_power c
A2: 5 = 6 - 1 ;
set i0 = [\c/];
set i1 = [/c\];

per cases ( [\c/] = [/c\] or not [\c/] = [/c\] ) ;

suppose [\c/] = [/c\] ; :: thesis: c ^2 < 2 to_power c

then c is Integer by INT_1:59;
then reconsider c = c as Element of NAT by A1, INT_1:16;
A3: (c + 1) ^2 < 2 to_power c by A1, Lm13;
c + 0 < c + 1 by XREAL_1:10;
then c ^2 < (c + 1) ^2 by SQUARE_1:78;
hence c ^2 < 2 to_power c by A3, XXREAL_0:2; :: thesis: verum

end;

suppose not [\c/] = [/c\] ; :: thesis: c ^2 < 2 to_power c

then A4: [\c/] + 1 = [/c\] by INT_1:66;
then A5: [\c/] = [/c\] - 1 ;
A6: [/c\] >= c by INT_1:def 5;
then reconsider i1 = [/c\] as Element of NAT by A1, INT_1:16;
i1 > 6 by A1, A6, XXREAL_0:2;
then A7: [\c/] > 5 by A2, A5, XREAL_1:11;
then reconsider i0 = [\c/] as Element of NAT by INT_1:16;
i0 >= 5 + 1 by A7, INT_1:20;
then A8: i1 ^2 < 2 to_power i0 by A4, Lm13;
i1 >= c by INT_1:def 5;
then i1 ^2 >= c ^2 by A1, SQUARE_1:77;
then A9: c ^2 < 2 to_power i0 by A8, XXREAL_0:2;
i0 <= c by INT_1:def 4;
then 2 to_power i0 <= 2 to_power c by PRE_FF:10;
hence c ^2 < 2 to_power c by A9, XXREAL_0:2; :: thesis: verum

end;

end;