theorem GRCY28: :: GROUP_18:4

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