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}

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

hence
gr {a} is cyclic Group
by GR_CY_1:def 7; :: thesis: verum
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;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