theorem Th11: :: BAGORD_2:13

for I being set holds 1. (finite-MultiSet_over I) = EmptyBag I