theorem Th30: :: NUMBER16:30

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