theorem :: NUMBER18:59

( Mersenne_Primes \/ Fermat_Primes is finite implies { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is finite ) by Problem90;