let p be Prime; :: thesis: not p * p is_a_product_of_two_different_primes
given p1, q1 being Prime such that A1: p1 <> q1 and
A2: p * p = p1 * q1 ; :: according to NUMBER07:def 5 :: thesis: contradiction
A3: p > 1 by INT_2:def 4;
A4: ( (p1 * p1) / p1 = p1 & (p1 * q1) / p1 = q1 ) by XCMPLX_1:89;
A5: ( (q1 * q1) / q1 = q1 & (p1 * q1) / q1 = p1 ) by XCMPLX_1:89;
p divides p * p ;
then ( p divides p1 or p divides q1 ) by A2, INT_5:7;

per cases then ( p = p1 or p = q1 ) by A3, INT_2:def 4;

suppose p = p1 ; :: thesis: contradiction

hence contradiction by A1, A2, A4; :: thesis: verum

end;

suppose p = q1 ; :: thesis: contradiction

hence contradiction by A1, A2, A5; :: thesis: verum

end;

end;