theorem InfiniteMersenne: :: NUMBER18:56

for n being Nat st n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 & n is not mersenne Prime holds
n + 1 is fermat Prime