let i, j be integer number ; :: thesis: for p being natural prime number holds
( not p divides i * j or p divides i or p divides j )
let p be natural prime number ; :: thesis: ( not p divides i * j or p divides i or p divides j )
assume A1: p divides i * j ; :: thesis: ( p divides i or p divides j )
assume not p divides i ; :: thesis: p divides j
then i gcd p = 1 by Th6;
hence p divides j by A1, INT_2:25, INT_2:def 3; :: thesis: verum