set p = Mersenne 11;
reconsider p = Mersenne 11 as non prime Nat by INT_2:def 4, GR_CY_3:22, NAT_D:9;
p is mersenne ;
hence ex b₁ being Nat st
( b₁ is mersenne & not b₁ is prime ) ; :: thesis: verum