given p, q being Prime such that A1: (p1 * p2) * p3 = p * q ; :: according to NUMBER09:def 3 :: thesis: contradiction
p1 * p2 divides (p1 * p2) * p3 ;
then ( p1 * p2 = 1 or p1 * p2 = p or p1 * p2 = q or p1 * p2 = p * q ) by A1, GR_CY_3:1;
then (p1 * p2) * 1 = p * q by A1;
then p3 = 1 by A1, XCMPLX_1:5;
hence contradiction by INT_2:def 4; :: thesis: verum