let n be non zero Nat; :: thesis: LP<=6n+1 n, primenumber (1 + (primeindex (LP<=6n+1 n))) are_not_twin
set LP = LP<=6n+1 n;
set s = primenumber (1 + (primeindex (LP<=6n+1 n)));
A1: LP<=6n+1 n <= primenumber (1 + (primeindex (LP<=6n+1 n))) by Th28;
(primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) <> 2 by Th30;
hence LP<=6n+1 n, primenumber (1 + (primeindex (LP<=6n+1 n))) are_not_twin by A1, Th6; :: thesis: verum