let p1, p2 be Prime; :: thesis: ( p1 <> p2 implies not p1 * p2 is having_exactly_one_prime_divisor )
assume A1: p1 <> p2 ; :: thesis: not p1 * p2 is having_exactly_one_prime_divisor
given p being Prime such that p divides p1 * p2 and
A2: for r being Prime st r <> p holds
not r divides p1 * p2 ; :: according to NUMBER08:def 6 :: thesis: contradiction
( p1 divides p1 * p2 & p2 divides p1 * p2 ) ;
then ( p1 = p & p2 = p ) by A2;
hence contradiction by A1; :: thesis: verum