theorem Th37: :: PRE_POLY:38

for X being set
for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)