theorem Th81: :: GROUP_1A:280

for G being addGroup
for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )