theorem Th11: :: RLTOPSP1:11
for X being non empty addLoopStr
for V1, V2, W1, W2 being Subset of X st V1 c= W1 & V2 c= W2 holds
V1 + V2 c= W1 + W2