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