theorem Th16: :: MORPH_01:16

for E being non empty addLoopStr
for A, B, C being Subset of E st B c= C holds
A + B c= A + C