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