theorem Th5: :: HILBASIS:5

for i, j being set
for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i holds
( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )