let n be Nat; :: thesis: ( n is prime implies not n is having_at_least_three_different_prime_divisors )
assume A1: n is prime ; :: 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 & q3 divides n ) ; :: according to NUMBER08:def 8 :: thesis: contradiction
( q1 = n & q2 = n & q3 = n ) by A1, A3, Th7;
hence contradiction by A2; :: thesis: verum