let i, j be Integer; :: thesis: for p being Prime holds
( not p divides i * j or p divides i or p divides j )
let p be Prime; :: 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