theorem :: NUMBER09:28

for n being Nat st n is even & n > 4 holds
(2 |^ n) - 1 is having_at_least_three_different_divisors