theorem Th30: :: NUMBER10:30

for n being non zero Nat holds (primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) >= 4