theorem Th16: :: NAT_4:16

for p being Prime
for a being Element of NAT st a <> 0 holds
( 1 <= p |^ (p |-count a) & p |^ (p |-count a) <= a )