A1: 1 + 1 <= m by NAT_2:29;
then A0: 1 < m by NAT_1:13;
1 <= n by NAT_1:14;
then 2 * 1 <= m * n by A1, XREAL_1:66;
hence 2 <= m * n ; :: according to NUMBER02:def 1 :: thesis: not m * n is prime
A7: n divides m * n ;
n <> m * n

proof

assume n = m * n ; :: thesis: contradiction
then 1 * n = m * n ;
hence contradiction by A0, XCMPLX_1:5; :: thesis: verum

end;

hence not m * n is prime by A7, NAT_2:def 1; :: thesis: verum