theorem Th2: :: GROUPP_1:2

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