theorem Th26: :: NUMBER16:26

for k being Nat holds 2 |^ k <= Product (primesFinS k)