theorem Th100: :: GROUP_3:100

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