let x be object ; :: thesis: ( x in Mersenne_Primes implies x is mersenne Prime )
assume x in Mersenne_Primes ; :: thesis: x is mersenne Prime
then consider n being Prime such that
A1: ( n = x & n is mersenne ) ;
thus x is mersenne Prime by A1; :: thesis: verum