theorem :: CONVEX1:40

for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {} by Lm8;