theorem :: NUMBER09:18

for a, n being Nat st a <> 1 & a <> n & not a is prime & a divides n holds
n is not_a_product_of_two_primes by GR_CY_3:1;