set X = { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ;
assume Z1: { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is infinite ; :: thesis: Mersenne_Primes \/ Fermat_Primes is infinite
set MFFP = Mersenne_Primes \/ Fermat_Primes;
assume G1: Mersenne_Primes \/ Fermat_Primes is finite ; :: thesis: contradiction
for m being Nat ex n being Nat st
( n >= m & n in Mersenne_Primes \/ Fermat_Primes )

proof

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in Mersenne_Primes \/ Fermat_Primes )
ex c being Nat st
( c > m & c > 8 & c in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } )

proof

assume for c being Nat holds
( not c > m or not c > 8 or not c in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ) ; :: thesis: contradiction
then Z3: for c being Nat holds
( not c in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } or c <= m or c <= 8 ) ;
{ n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } c= Seg m

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } or x in Seg m )
assume Z4: x in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ; :: thesis: x in Seg m
then consider nn being Nat such that
Z2: ( x = nn & nn > 8 & card (PrimeDivisors nn) = 1 & card (PrimeDivisors (nn + 1)) = 1 ) ;
nn <> 0

proof

assume nn = 0 ; :: thesis: contradiction
hence contradiction by Z2; :: thesis: verum

end;

then Z5: 1 <= nn by NAT_1:14;
nn <= m by Z2, Z3, Z4;
hence x in Seg m by Z2, Z5; :: thesis: verum

end;

hence contradiction by Z1; :: thesis: verum

end;

then consider c being Nat such that
B1a: ( c > m & c > 8 & c in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ) ;
B1: ( c > m & c > 8 & c in { n where n is Nat : ( n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } ) by B1a;
consider mm being Nat such that
B3: ( mm = c & mm > 8 & card (PrimeDivisors mm) = 1 & card (PrimeDivisors (mm + 1)) = 1 ) by B1;
( c is mersenne Prime or c + 1 is fermat Prime ) by B3, InfiniteMersenne;
then D2: ( c in Mersenne_Primes \/ Fermat_Primes or c + 1 in Mersenne_Primes \/ Fermat_Primes ) by LemmaA, LemmaB;
c + 1 > c by NAT_1:16;
then ( c > m & c + 1 > m ) by B1, XXREAL_0:2;
hence ex n being Nat st
( n >= m & n in Mersenne_Primes \/ Fermat_Primes ) by D2; :: thesis: verum

end;

hence contradiction by G1, PYTHTRIP:9; :: thesis: verum