for G being addGroup
for g being Element of G
for A being Subset of G holds A * g in con_class A