let G be Group; :: thesis:
let G1 be Subgroup of G; :: thesis:
let a be Element of G; :: thesis:
let a1 be Element of G1; :: thesis:
reconsider Gr = gr {a1} as Subgroup of G by GROUP_2:56;
assume A1: a = a1 ; :: thesis:
A2: for b being Element of G st b in Gr holds
b in gr {a}

let b be Element of G; :: thesis:
assume A3: b in Gr ; :: thesis:
then b in G1 by GROUP_2:40;
then reconsider b1 = b as Element of G1 by STRUCT_0:def 5;
consider i being Integer such that
A4: b1 = a1 |^ i by A3, GR_CY_1:5;
b = a |^ i by A1, A4, GROUP_4:2;
hence b in gr {a} by GR_CY_1:5; :: thesis:

end;

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

let b be Element of G; :: thesis:
assume b in gr {a} ; :: thesis:
then consider i being Integer such that
A5: b = a |^ i by GR_CY_1:5;
b = a1 |^ i by A1, A5, GROUP_4:2;
hence b in Gr by GR_CY_1:5; :: thesis:

end;