let n be Nat; :: thesis: ( n is having_at_least_three_different_prime_divisors implies n is having_at_least_three_different_divisors )
given q1, q2, q3 being Prime such that A1: ( q1,q2,q3 are_mutually_distinct & q1 divides n & q2 divides n & q3 divides n ) ; :: according to NUMBER08:def 8 :: thesis: n is having_at_least_three_different_divisors
( q1 > 1 & q2 > 1 & q3 > 1 ) by INT_2:def 4;
hence n is having_at_least_three_different_divisors by A1; :: thesis: verum