for p being prime Nat
for n, m being Nat st n divides p |^ m holds
ex r being Nat st
( n = p |^ r & r <= m )