for p, q being Prime
for k being Nat holds
( not k divides p * q or k = 1 or k = p or k = q or k = p * q )