theorem Fer1: :: NUMBER18:47
( card (PrimeDivisors 1) = 1 & card (PrimeDivisors (1 + 1)) = 1 & 1 is not mersenne Prime implies 1 + 1 is fermat Prime )