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

proof

a in gr {a} by Th2;
then reconsider a1 = a as Element of (gr {a}) by STRUCT_0:def 5;
take a1 ; :: thesis: gr {a} = gr {a1}
thus gr {a} = gr {a1} by Th3; :: thesis: verum

end;

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