for m, n being Nat holds
( not m * n is even or m is even or n is even ) ;