let G be strict Group; :: thesis: for b being Element of G holds

( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

let b be Element of G; :: thesis: ( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

thus ( ( for a being Element of G ex i being Integer st a = b |^ i ) implies G = gr {b} ) :: thesis: ( G = gr {b} implies for a being Element of G ex i being Integer st a = b |^ i )

let a be Element of G; :: thesis: ex i being Integer st a = b |^ i

a in gr {b} by A2, STRUCT_0:def 5;

hence ex i being Integer st a = b |^ i by GR_CY_1:5; :: thesis: verum

( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

let b be Element of G; :: thesis: ( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

thus ( ( for a being Element of G ex i being Integer st a = b |^ i ) implies G = gr {b} ) :: thesis: ( G = gr {b} implies for a being Element of G ex i being Integer st a = b |^ i )

proof

assume A2:
G = gr {b}
; :: thesis: for a being Element of G ex i being Integer st a = b |^ i
assume A1:
for a being Element of G ex i being Integer st a = b |^ i
; :: thesis: G = gr {b}

for a being Element of G holds a in gr {b}

end;for a being Element of G holds a in gr {b}

proof

hence
G = gr {b}
by GROUP_2:62; :: thesis: verum
let a be Element of G; :: thesis: a in gr {b}

ex i being Integer st a = b |^ i by A1;

hence a in gr {b} by GR_CY_1:5; :: thesis: verum

end;ex i being Integer st a = b |^ i by A1;

hence a in gr {b} by GR_CY_1:5; :: thesis: verum

let a be Element of G; :: thesis: ex i being Integer st a = b |^ i

a in gr {b} by A2, STRUCT_0:def 5;

hence ex i being Integer st a = b |^ i by GR_CY_1:5; :: thesis: verum