3 = Mersenne 2 by GR_CY_3:18;
hence ( card (PrimeDivisors 3) = 1 & card (PrimeDivisors (3 + 1)) = 1 & 3 is not mersenne Prime implies 3 + 1 is fermat Prime ) by XPRIMES1:3; :: thesis: verum