set A = { [p,q] where p, q is Prime : p,q are_not_twin } ;
deffunc H₁( non zero Nat) -> Prime = LP<=6n+1 $1;
deffunc H₂( non zero Nat) -> object = [H₁($1),(primenumber (1 + (primeindex H₁($1))))];
defpred S₁[ Nat, object ] means ex n being non zero Nat st
( n = $1 & $2 = H₂(n) );
set P = 6n+1_Primes ;
deffunc H₃( Element of 6n+1_Primes ) -> Element of NAT = In ((($1 - 1) div 6),NAT);
consider C being Function of 6n+1_Primes,NAT such that
A1: for p being Element of 6n+1_Primes holds C . p = H₃(p) from FUNCT_2:sch 4();
A2: dom C = 6n+1_Primes by FUNCT_2:def 1;

A3: now :: thesis: for p being Element of 6n+1_Primes holds 6 * ((p - 1) div 6) = p - 1

let p be Element of 6n+1_Primes ; :: thesis: 6 * ((p - 1) div 6) = p - 1
p in 6n+1_Primes ;
then ex n being Nat st
( p = (6 * n) + 1 & (6 * n) + 1 is prime ) ;
hence 6 * ((p - 1) div 6) = p - 1 by NAT_D:18; :: thesis: verum

end;

C is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 C or not x2 in proj1 C or not C . x1 = C . x2 or x1 = x2 )
assume that
A4: x1 in dom C and
A5: x2 in dom C and
A6: C . x1 = C . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of 6n+1_Primes by A4, A5;
( C . x1 = H₃(x1) & C . x2 = H₃(x2) ) by A1;
then A7: 6 * ((x1 - 1) div 6) = 6 * ((x2 - 1) div 6) by A6;
( 6 * ((x1 - 1) div 6) = x1 - 1 & 6 * ((x2 - 1) div 6) = x2 - 1 ) by A3;
hence x1 = x2 by A7; :: thesis: verum

end;

then reconsider D = rng C as infinite Subset of NAT by A2, CARD_1:59, RELAT_1:def 19;
A8: for d being Element of D holds (6 * d) + 1 is prime

proof

let d be Element of D; :: thesis: (6 * d) + 1 is prime
consider p being Element of 6n+1_Primes such that
A9: d = C . p by FUNCT_2:113;
A10: H₃(p) = (p - 1) div 6 ;
p in 6n+1_Primes ;
then A11: ex n being Nat st
( p = (6 * n) + 1 & (6 * n) + 1 is prime ) ;
6 * ((p - 1) div 6) = p - 1 by A3;
hence (6 * d) + 1 is prime by A1, A9, A10, A11; :: thesis: verum

end;

A12: now :: thesis: for d being Element of D holds not d = 0

let d be Element of D; :: thesis: not d = 0
assume d = 0 ; :: thesis: contradiction
then (6 * 0) + 1 is prime by A8;
hence contradiction ; :: thesis: verum

end;

A13: for i being Element of D ex j being object st S₁[i,j]

proof

let i be Element of D; :: thesis: ex j being object st S₁[i,j]
reconsider a = i as non zero Nat by A12;
take H₂(a) ; :: thesis: S₁[i,H₂(a)]
thus S₁[i,H₂(a)] ; :: thesis: verum

end;

consider f being ManySortedSet of D such that
A14: for d being Element of D holds S₁[d,f . d] from PBOOLE:sch 6(A13);
A15: dom f = D by PARTFUN1:def 2;
A16: rng f c= { [p,q] where p, q is Prime : p,q are_not_twin }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { [p,q] where p, q is Prime : p,q are_not_twin } )
assume y in rng f ; :: thesis: y in { [p,q] where p, q is Prime : p,q are_not_twin }
then consider k being object such that
A17: k in dom f and
A18: f . k = y by FUNCT_1:def 3;
reconsider k = k as non zero Element of NAT by A12, A15, A17;
A19: S₁[k,f . k] by A14, A17;
H₁(k), primenumber (1 + (primeindex H₁(k))) are_not_twin by Th31;
hence y in { [p,q] where p, q is Prime : p,q are_not_twin } by A18, A19; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A20: x1 in dom f and
A21: x2 in dom f and
A22: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1 as non zero Nat by A12, A20;
reconsider x2 = x2 as non zero Nat by A12, A21;
( S₁[x1,f . x1] & S₁[x2,f . x2] ) by A14, A20, A21;
then A23: H₁(x1) = H₁(x2) by A22, XTUPLE_0:1;
( (6 * x1) + 1 is prime & (6 * x2) + 1 is prime ) by A8, A20, A21;
hence x1 = x2 by A23, Th34; :: thesis: verum

end;

hence { [p,q] where p, q is Prime : p,q are_not_twin } is infinite by A15, A16, CARD_1:59; :: thesis: verum