theorem Th16: :: NUMBER13:16

for k being Nat
for p being Prime st p, Product (primesFinS k) are_coprime holds
primenumber k <= p