ex n being Nat st
( n divides p * q & n <> 1 & n <> p * q )

proof

take p ; :: thesis: ( p divides p * q & p <> 1 & p <> p * q )
thus p divides p * q ; :: thesis: ( p <> 1 & p <> p * q )
thus p <> 1 by INT_2:def 4; :: thesis: p <> p * q
assume p = p * q ; :: thesis: contradiction
then p * q = p * 1 ;
then q = 1 by XCMPLX_1:5;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence not p * q is prime ; :: thesis: verum