theorem LtPrimenumber: :: PRIMRECI:12

for n being Nat
for p being Prime st p < primenumber (n + 1) holds
p <= primenumber n