theorem Th34: :: PRE_POLY:35

for X being set
for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)