theorem Th31: :: NUMBER10:31

for n being non zero Nat holds LP<=6n+1 n, primenumber (1 + (primeindex (LP<=6n+1 n))) are_not_twin