reconsider p = Mersenne 2 as Prime by PEPIN:41, GR_CY_3:18;
p is mersenne ;
hence ex b₁ being Prime st b₁ is mersenne ; :: thesis: verum