theorem :: NUMBER09:27

for n being Nat st n is having_at_least_three_different_prime_divisors holds
not n is_a_product_of_two_different_primes ;