theorem Th17: :: GR_CY_1:17

for G being Group holds
( G is cyclic Group iff ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 )