for i being Nat st i is prime holds
for m, n being Nat holds
( not i divides m * n or i divides m or i divides n )