theorem Th1: :: BAGORD_2:12

for a being object
for I being set holds
( a is multiset of I iff a is bag of I )