theorem Th5: :: GLIB_004:5

for A being set
for b1, b2 being Rbag of A st ( for x being set st x in A holds
b1 . x <= b2 . x ) holds
Sum b1 <= Sum b2