theorem :: NUMBER13:23

for k being Nat st 3 <= k holds
(primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)