theorem Th77: :: NUMBER08:77

for p1, p2 being Prime st p1 <> p2 holds
not p1 * p2 is having_exactly_one_prime_divisor