set X = { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ;
for x being object st x in { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } holds
x is natural

proof

let x be object ; :: thesis: ( x in { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } implies x is natural )
assume x in { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ; :: thesis: x is natural
then consider xx being Nat such that
B1: ( xx = x & card (PrimeDivisors xx) = 1 & card (PrimeDivisors (xx + 1)) = 1 ) ;
thus x is natural by B1; :: thesis: verum

end;

then AA: { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is natural-membered by MEMBERED:def 6;
assume { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is finite ; :: thesis: Mersenne_Primes \/ Fermat_Primes is finite
then consider nn being Nat such that
AB: { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } c= Segm nn by AA, AFINSQ_2:2;
set Y = Mersenne_Primes \/ Fermat_Primes;
assume Mersenne_Primes \/ Fermat_Primes is infinite ; :: thesis: contradiction
then consider c being Nat such that
F1: ( c > nn & c in Mersenne_Primes \/ Fermat_Primes ) by Infinite;
0 + 1 <= c by F1, NAT_1:13;
then GG: c - 1 in NAT by INT_1:5;
( c in Mersenne_Primes or c in Fermat_Primes ) by XBOOLE_0:def 3, F1;

per cases then ( c is mersenne Prime or c is fermat Prime ) by LemmaMer, LemmaFer;

suppose c is mersenne Prime ; :: thesis: contradiction

then ( card (PrimeDivisors c) = 1 & card (PrimeDivisors (c + 1)) = 1 ) by MersenneDivisors;
then c in { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ;
then c in Segm nn by AB;
hence contradiction by F1, NAT_1:44; :: thesis: verum

end;

suppose c is fermat Prime ; :: thesis: contradiction

then G1: ( card (PrimeDivisors c) = 1 & card (PrimeDivisors (c - 1)) = 1 ) by FermatDivisors;
(c - 1) + 1 = c ;
then c - 1 in { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } by GG, G1;
then c - 1 < nn by AB, NAT_1:44;
then (c - 1) + 1 <= nn by NAT_1:13;
hence contradiction by F1; :: thesis: verum

end;

end;