assume A1: ( card (PrimeDivisors 1) = 1 & card (PrimeDivisors (1 + 1)) = 1 ) ; :: thesis: ( 1 is mersenne Prime or 1 + 1 is fermat Prime )
card (PrimeDivisors 1) = 0 by ZeroDiv1;
hence ( 1 is mersenne Prime or 1 + 1 is fermat Prime ) by A1; :: thesis: verum