theorem :: NUMBER10:38

for n being Nat st n > 4 holds
ex m being Nat st
( n < m & m < 2 * n & m is_a_product_of_two_different_primes )