let G be Group; :: thesis: for a being Element of G holds a in gr {a}
let a be Element of G; :: thesis: a in gr {a}
ex i being Integer st a = a |^ i
proof
reconsider i = 1 as Integer ;
take i ; :: thesis: a = a |^ i
thus a = a |^ i by GROUP_1:26; :: thesis: verum
end;
hence a in gr {a} by GR_CY_1:5; :: thesis: verum