A1: 2 <= m by NUMBER02:def 1;
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

per cases ( n = 1 or n <> 1 ) ;

suppose n = 1 ; :: thesis: not m * n is prime

hence not m * n is prime ; :: thesis: verum

end;

suppose A8: n <> 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 ;
then m = 1 by XCMPLX_1:5;
hence contradiction by NUMBER02:def 1; :: thesis: verum

end;

hence not m * n is prime by A7, A8; :: thesis: verum

end;

end;