theorem Th27: :: NUMBER16:27

for n being Nat st 2 <= n holds
ex k being non zero Nat st
( Product (primesFinS k) <= n & n < Product (primesFinS (k + 1)) )