theorem :: GROUP_1A:286

for G being addGroup
for a being Element of G
for A being Subset of G holds (con_class a) + A = A + (con_class a)