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