let n be Nat; :: thesis: ( n is having_exactly_one_prime_divisor implies not n is having_at_least_three_different_prime_divisors )
given p being Prime such that p divides n and
A1: for r being Prime st r <> p holds
not r divides n ; :: according to NUMBER08:def 6 :: thesis: not n is having_at_least_three_different_prime_divisors
given q1, q2, q3 being Prime such that A2: q1,q2,q3 are_mutually_distinct and
A3: ( q1 divides n & q2 divides n ) and
q3 divides n ; :: according to NUMBER08:def 8 :: thesis: contradiction
( q1 = p & q2 = p ) by A1, A3;
hence contradiction by A2; :: thesis: verum