let x be Real; :: thesis:
assume A1: x > 9 ; :: thesis:
set n = [/x\];
A2: [/x\] >= x by INT_1:def 7;
then reconsider n = [/x\] as Element of NAT by A1, INT_1:3;
2 * n >= 2 * x by A2, XREAL_1:64;
then A3: (2 * n) ^2 >= (2 * x) * (2 * x) by A1, Lm20;
n > 9 by A1, A2, XXREAL_0:2;
then n >= 9 + 1 by NAT_1:13;
then A4: 2 to_power (n - 1) > (2 * n) ^2 by Lm28;
[/x\] - [\x/] <= 1

proof

per cases ;

suppose x is Integer ; :: thesis:

then [\x/] = [/x\] by INT_1:34;
hence [/x\] - [\x/] <= 1 ; :: thesis:

end;

suppose x is not Integer ; :: thesis:

then not [\x/] = [/x\] by INT_1:34;
then [\x/] + 1 = [/x\] by INT_1:41;
hence [/x\] - [\x/] <= 1 ; :: thesis:

end;

end;

end;

then [/x\] <= 1 + [\x/] by XREAL_1:20;
then [\x/] >= n - 1 by XREAL_1:20;
then A5: 2 to_power [\x/] >= 2 to_power (n - 1) by PRE_FF:8;
x >= [\x/] by INT_1:def 6;
then 2 to_power x >= 2 to_power [\x/] by PRE_FF:8;
then 2 to_power x >= 2 to_power (n - 1) by A5, XXREAL_0:2;
then 2 to_power x > (2 * n) ^2 by A4, XXREAL_0:2;
hence 2 to_power x > (2 * x) ^2 by A3, XXREAL_0:2; :: thesis: