theorem Th15: :: NUMBER13:15

for k being Nat
for p being Prime st p < primenumber k holds
p in rng (primesFinS k)