theorem :: NUMBER18:55

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