let G be strict Group; :: thesis: 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 )
let a be Element of G; :: thesis: ( G = gr {a} implies for H being strict Subgroup of G st H <> (1). G holds
ex k being Nat st
( 0 < k & a |^ k in H ) )
assume A1: G = gr {a} ; :: thesis: for H being strict Subgroup of G st H <> (1). G holds
ex k being Nat st
( 0 < k & a |^ k in H )
let H be strict Subgroup of G; :: thesis: ( H <> (1). G implies ex k being Nat st
( 0 < k & a |^ k in H ) )
assume H <> (1). G ; :: thesis: ex k being Nat st
( 0 < k & a |^ k in H )
then A2: H <> (1). H by GROUP_2:63;
consider c being Element of H such that
A3: c <> 1_ H by A2, Th23;
A4: c in H ;
then c in G by GROUP_2:40;
then reconsider c = c as Element of G ;
A5: c in gr {a} by A1;
ex j being Integer st
( c = a |^ j & j <> 0 ) then consider j being Integer such that
A9: c = a |^ j and
A10: j <> 0 ;
consider n being Nat such that
A11: ( j = n or j = - n ) by INT_1:2;