A1: 2 <= m by Def1;
2 <= n by Def1;
then 2 * 2 <= m * n by A1, XREAL_1:66;
hence 2 <= m * n by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not m * n is prime
assume A2: m * n is prime ; :: thesis: contradiction
n divides m * n ;
then ( n = 1 or 1 * n = m * n ) by A2;
hence contradiction by A2; :: thesis: verum