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