A1: 1 = 2 - 1 ;
let n be Nat; :: thesis: ( n >= 2 implies not (2 to_power n) - 1 in POWEROF2SET )
assume n >= 2 ; :: thesis: not (2 to_power n) - 1 in POWEROF2SET
then n - 1 >= 1 by A1, XREAL_1:9;
then (2 to_power ((n + (- 1)) + 1)) - (2 to_power (n - 1)) > 1 by Lm48;
then 2 to_power n > 1 + (2 to_power (n - 1)) by XREAL_1:20;
then A3: (2 to_power n) - 1 > 2 to_power (n - 1) by XREAL_1:20;
assume (2 to_power n) - 1 in POWEROF2SET ; :: thesis: contradiction
then consider m being Element of NAT such that
A4: 2 to_power m = (2 to_power n) - 1 ;

now :: thesis: not m >= n

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

end;

then m + 1 <= n by INT_1:7;
then A6: m <= n - 1 by XREAL_1:19;
m >= n - 1 by A4, A3, POWER:39;
hence contradiction by A4, A3, A6, XXREAL_0:1; :: thesis: verum