theorem :: NUMBER08:80

for n being Nat st n is having_exactly_one_prime_divisor holds
not n is having_at_least_three_different_prime_divisors