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 ;
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 ;
A8: a |^ i <> 1_ G by ;
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 ;
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;