5 = Fermat 1 by PEPIN:51;
hence ( card (PrimeDivisors 4) = 1 & card (PrimeDivisors (4 + 1)) = 1 & 4 is not mersenne Prime implies 4 + 1 is fermat Prime ) by XPRIMES1:5; :: thesis: verum