theorem :: RUSUB_5:6

for V being non empty addLoopStr
for M, N being non empty Subset of V holds not M + N is empty