theorem Fer7: :: NUMBER18:53
( card (PrimeDivisors 7) = 1 & card (PrimeDivisors (7 + 1)) = 1 & 7 is not mersenne Prime implies 7 + 1 is fermat Prime )