theorem :: GROUP_8:14

for G being strict Group st ex a being Element of G st a <> 1_ G holds
( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) )