theorem :: GROUP_8:1

for p being Element of NAT
for G being finite strict Group st p is prime & card G = p holds
ex a being Element of G st ord a = p