:: deftheorem defines + GROUP_1A:def 13 :
for G being non empty addMagma
for g being Element of G
for A being Subset of G holds g + A = {g} + A;