theorem Th100: :: GROUP_1A:299

for G being addGroup
for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }