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