theorem :: NUMBER09:20

for c being Nat st c is_a_product_of_two_different_primes holds
c is a_product_of_two_primes ;