let n be Nat; :: thesis: ( n is zero implies n is having_at_least_three_different_prime_divisors )
assume A1: n is zero ; :: thesis: n is having_at_least_three_different_prime_divisors
take P2 ; :: according to NUMBER08:def 8 :: thesis: ex q2, q3 being Prime st
( P2,q2,q3 are_mutually_distinct & P2 divides n & q2 divides n & q3 divides n )
take P3 ; :: thesis: ex q3 being Prime st
( P2,P3,q3 are_mutually_distinct & P2 divides n & P3 divides n & q3 divides n )
take P5 ; :: thesis: ( P2,P3,P5 are_mutually_distinct & P2 divides n & P3 divides n & P5 divides n )
thus ( P2,P3,P5 are_mutually_distinct & P2 divides n & P3 divides n & P5 divides n ) by A1, NAT_D:6; :: thesis: verum