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 )

A9: c = a |^ j and

A10: j <> 0 ;

consider n being Nat such that

A11: ( j = n or j = - n ) by INT_1:2;

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

then consider j being Integer such that
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;( 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

A9: c = a |^ j and

A10: j <> 0 ;

consider n being Nat such that

A11: ( j = n or j = - n ) by INT_1:2;