theorem :: BAGORD_2:16

for I being set
for M being RelExtension of finite-MultiSet_over I holds the carrier of M = Bags I