let a be mersenne Prime; :: thesis: a in Mersenne_Primes \/ Fermat_Primes
a in Mersenne_Primes ;
hence a in Mersenne_Primes \/ Fermat_Primes by XBOOLE_0:def 3; :: thesis: verum