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 Element of 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 Element of 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 Element of NAT st
( 0 < k & a |^ k in H )
let H be strict Subgroup of G; :: thesis: ( H <> (1). G implies ex k being Element of NAT st
( 0 < k & a |^ k in H ) )
assume A2: H <> (1). G ; :: thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )
A3: H <> (1). H by A2, GROUP_2:75;
consider b being Element of H;
consider c being Element of H such that
A4: c <> 1_ H by A3, Th23;
A5: c in H by STRUCT_0:def 5;
then c in G by GROUP_2:49;
then reconsider c = c as Element of G by STRUCT_0:def 5;
A6: c in gr {a} by A1, STRUCT_0:def 5;
ex j being Integer st
( c = a |^ j & j <> 0 )

proof

assume A7: for j being Integer holds
( not c = a |^ j or not j <> 0 ) ; :: thesis: contradiction
consider i being Integer such that
A8: c = a |^ i by A6, GR_CY_1:25;
A9: a |^ i <> 1_ G by A4, A8, GROUP_2:53;
i = 0 by A7, A8;
hence contradiction by A9, GROUP_1:59; :: thesis: verum

end;

then consider j being Integer such that
A10: ( c = a |^ j & j <> 0 ) ;
consider n being Element of NAT such that
A11: ( j = n or j = - n ) by INT_1:8;

per cases ( j = n or j = - n ) by A11;

suppose A12: j = n ; :: thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )

thus ex k being Element of NAT st
( 0 < k & a |^ k in H ) by A5, A10, A12; :: thesis: verum

end;

suppose A13: j = - n ; :: thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )

then n <> 0 by A10;
then A14: 0 < n ;
(a |^ n) " in H by A5, A10, A13, GROUP_1:71;
then ((a |^ n) " ) " in H by GROUP_2:60;
then a |^ n in H by GROUP_1:19;
hence ex k being Element of NAT st
( 0 < k & a |^ k in H ) by A14; :: thesis: verum

end;

end;