:: deftheorem defines a_product_of_three_different_primes NUMBER10:def 6 :
for c being Complex holds
( c is a_product_of_three_different_primes iff ex p, q, r being Prime st
( p,q,r are_mutually_distinct & c = (p * q) * r ) );