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

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

hence
contradiction
by A1; :: thesis: verum
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;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