theorem :: NUMBER12:15
for A being set st A = { n where n is non zero Nat : n gcd ((2 |^ n) - 1) > 1 } holds
( A is infinite & ( for k being Nat st k in A holds
k >= 6 ) )