theorem Th8: :: NAT_6:8

for x, p being Prime
for k being non zero Nat holds
( x divides p |^ k iff x = p )