let n be Element of NAT ; :: thesis: ( n >= 2 implies not (2 to_power n) - 1 in POWEROF2SET )
assume A1: n >= 2 ; :: thesis: not (2 to_power n) - 1 in POWEROF2SET
A2: 1 = 2 - 1 ;
assume (2 to_power n) - 1 in POWEROF2SET ; :: thesis: contradiction
then consider m being Element of NAT such that
A3: 2 to_power m = (2 to_power n) - 1 ;

A4: now

assume m >= n ; :: thesis: contradiction
then A5: 2 to_power m >= 2 to_power n by PRE_FF:10;
(2 to_power n) + 1 > (2 to_power n) + 0 by XREAL_1:8;
hence contradiction by A3, A5, XREAL_1:21; :: thesis: verum

end;

A6: n - 1 >= 1 by A1, A2, XREAL_1:11;
then n - 1 is Element of NAT by INT_1:16;
then (2 to_power ((n + (- 1)) + 1)) - (2 to_power (n - 1)) > 1 by A6, Lm56;
then 2 to_power n > 1 + (2 to_power (n - 1)) by XREAL_1:22;
then A7: (2 to_power n) - 1 > 2 to_power (n - 1) by XREAL_1:22;
then A8: m >= n - 1 by A3, POWER:44;
m + 1 <= n by A4, INT_1:20;
then m <= n - 1 by XREAL_1:21;
hence contradiction by A3, A7, A8, XXREAL_0:1; :: thesis: verum