:: deftheorem defines -bag MOEBIUS3:def 7 :
for A being finite Subset of SetPrimes holds A -bag = (EmptyBag SetPrimes) +* (id A);