3 is fermat Prime by XPRIMES1:3, PEPIN:50;
hence ( card (PrimeDivisors 2) = 1 & card (PrimeDivisors (2 + 1)) = 1 & 2 is not mersenne Prime implies 2 + 1 is fermat Prime ) ; :: thesis: verum