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