theorem Problem90: :: NUMBER18:58
( { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is infinite implies Mersenne_Primes \/ Fermat_Primes is infinite )