let G be Group; :: thesis: for a being Element of G st a <> 1_ G holds
gr {a} <> (1). G
let a be Element of G; :: thesis: ( a <> 1_ G implies gr {a} <> (1). G )
assume A1: a <> 1_ G ; :: thesis: gr {a} <> (1). G
assume A2: gr {a} = (1). G ; :: thesis: contradiction
A3: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def 7;
A4: {a} c= the carrier of (gr {a}) by GROUP_4:def 4;
for xx being set st xx = a holds
xx = 1_ G

proof

let xx be set ; :: thesis: ( xx = a implies xx = 1_ G )
assume xx = a ; :: thesis: xx = 1_ G
then xx in {a} by TARSKI:def 1;
hence xx = 1_ G by A2, A3, A4, TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum