theorem :: PRE_POLY:75

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