for n being Nat
for a being non trivial Nat
for p being prime Nat st a divides p |^ n holds
p divides a