:: deftheorem defines + MATHMORP:def 1 :
for T being non empty addMagma
for p being Element of T
for X being Subset of T holds X + p = { (q + p) where q is Element of T : q in X } ;