theorem Th7: :: GR_CY_2:7

for G being strict Group
for a being Element of G st G is finite & G = gr {a} holds
for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}