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 )

proof

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

end;

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;

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

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

hence ex k being Nat st
( 0 < k & a |^ k in H ) by A4, A9, A10; :: thesis: verum

end;

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

then A13: 0 < n by A10;
(a |^ n) " in H by A4, A9, A12, GROUP_1:36;
then ((a |^ n) ") " in H by GROUP_2:51;
hence ex k being Nat st
( 0 < k & a |^ k in H ) by A13; :: thesis: verum

end;

end;