theorem Th11: :: GR_CY_2:11

for k, n, p being Element of NAT
for G being finite Group
for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p