let G be addGroup; :: thesis: for a being Element of G holds
( con_class a = {(0_ G)} iff a = 0_ G )
let a be Element of G; :: thesis: ( con_class a = {(0_ G)} iff a = 0_ G )
thus ( con_class a = {(0_ G)} implies a = 0_ G ) :: thesis: ( a = 0_ G implies con_class a = {(0_ G)} )

proof

assume A1: con_class a = {(0_ G)} ; :: thesis: a = 0_ G
a in con_class a by Th81;
hence a = 0_ G by A1, TARSKI:def 1; :: thesis: verum

end;

assume A2: a = 0_ G ; :: thesis: con_class a = {(0_ G)}
thus con_class a c= {(0_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(0_ G)} c= con_class a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class a or x in {(0_ G)} )
assume x in con_class a ; :: thesis: x in {(0_ G)}
then consider b being Element of G such that
A3: b = x and
A4: a,b are_conjugated by Th80;
b = 0_ G by A2, A4, ThB78;
hence x in {(0_ G)} by A3, TARSKI:def 1; :: thesis: verum

end;

thus {(0_ G)} c= con_class a by A2, Th81, ZFMISC_1:31; :: thesis: verum