theorem :: NUMBER10:39

for n being Nat st n > 15 holds
ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes )