for G being finite Group holds
( G is cyclic iff ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n )