let m, n be Nat; :: thesis: ( m >= 2 & n >= 2 implies m * n is composite )
assume A1: 2 <= m ; :: thesis: ( not n >= 2 or m * n is composite )
assume A2: 2 <= n ; :: thesis: m * n is composite
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
ex N being Nat st
( N divides m * n & N <> 1 & N <> m * n )

proof

take m ; :: thesis: ( m divides m * n & m <> 1 & m <> m * n )
thus m divides m * n ; :: thesis: ( m <> 1 & m <> m * n )
thus m <> 1 by A1; :: thesis: m <> m * n
assume m = m * n ; :: thesis: contradiction
then m * n = m * 1 ;
then n = 1 by A1, XCMPLX_1:5;
hence contradiction by A2; :: thesis: verum

end;

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