let G be Group; :: thesis: for a being Element of holds gr {a} is cyclic Group
let a be Element of ; :: thesis: gr {a} is cyclic Group
ex a1 being Element of st gr {a} = gr {a1}

proof

a in gr {a} by Th8;
then reconsider a1 = a as Element of by STRUCT_0:def 5;
take a1 ; :: thesis: gr {a} = gr {a1}
thus gr {a} = gr {a1} by Th9; :: thesis: verum

end;

hence gr {a} is cyclic Group by GR_CY_1:def 9; :: thesis: verum