for G being finite commutative Group
for p being Prime
for m being Nat
for a being Element of G st card G = p |^ m & a <> 1_ G holds
ex n being Nat st ord a = p |^ (n + 1)