theorem Th24: :: GROUP_8:24
for G being strict Group
for a being Element of G st G = gr {a} holds
for H being strict Subgroup of G st H <> (1). G holds
ex k being Nat st
( 0 < k & a |^ k in H )