set a = p1 |^ m;
set b = p2 |^ n;
given q1, q2, q3 being Prime such that A1: q1,q2,q3 are_mutually_distinct and
A2: ( q1 divides (p1 |^ m) * (p2 |^ n) & q2 divides (p1 |^ m) * (p2 |^ n) & q3 divides (p1 |^ m) * (p2 |^ n) ) ; :: according to NUMBER08:def 8 :: thesis: contradiction
( ( q1 divides p1 |^ m or q1 divides p2 |^ n ) & ( q2 divides p1 |^ m or q2 divides p2 |^ n ) & ( q3 divides p1 |^ m or q3 divides p2 |^ n ) ) by A2, INT_5:7;
then ( ( q1 = p1 or q1 = p2 ) & ( q2 = p1 or q2 = p2 ) & ( q3 = p1 or q3 = p2 ) ) by Th7, NAT_3:5;
hence contradiction by A1; :: thesis: verum