:: deftheorem defines + RUSUB_4:def 8 :
for V being non empty addLoopStr
for M being Subset of V
for v being Element of V holds v + M = { (v + u) where u is Element of V : u in M } ;