theorem Th8: :: RUSUB_5:8

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