theorem Th8: :: GR_CY_2:8

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