theorem Th7: :: INT_5:7
for i, j being Integer
for p being Prime holds
( not p divides i * j or p divides i or p divides j )