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