assume A1: ( card (PrimeDivisors 6) = 1 & card (PrimeDivisors (6 + 1)) = 1 ) ; :: thesis: ( 6 is mersenne Prime or 6 + 1 is fermat Prime )
card (PrimeDivisors (2 * 3)) = 2 by XPRIMES1:2, XPRIMES1:3, Moshe1;
hence ( 6 is mersenne Prime or 6 + 1 is fermat Prime ) by A1; :: thesis: verum