theorem Th29: :: NUMBER10:29
for n being non zero Nat holds primenumber (1 + (primeindex (LP<=6n+1 n))) >= (6 * n) + 5