let p, q be Prime; :: thesis: for k being Nat holds
( not k divides p * q or k = 1 or k = p or k = q or k = p * q )
let k be Nat; :: thesis: ( not k divides p * q or k = 1 or k = p or k = q or k = p * q )
assume A1: k divides p * q ; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

per cases ( k,p are_coprime or k gcd p = p ) by PEPIN:2;

suppose k,p are_coprime ; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

then k divides q by A1, PEPIN:3;
hence ( k = 1 or k = p or k = q or k = p * q ) by INT_2:def 4; :: thesis: verum

end;

suppose k gcd p = p ; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

then p divides k by NAT_D:def 5;
then consider l being Nat such that
A2: k = p * l by NAT_D:def 3;
consider m being Nat such that
A3: k * m = p * q by A1, NAT_D:def 3;
p * (l * m) = p * q by A2, A3;
then l * m = q by XCMPLX_1:5;
then l divides q by NAT_D:def 3;
then ( l = 1 or l = q ) by INT_2:def 4;
hence ( k = 1 or k = p or k = q or k = p * q ) by A2; :: thesis: verum

end;

end;