theorem :: GROUP_3:87
for G being Group
for a being Element of G
for A being Subset of G holds (con_class a) * A = A * (con_class a)