for n being Nat st n >= 2 holds
not (2 to_power n) - 1 in POWEROF2SET by Lm49;