theorem :: MOEBIUS3:54

for A being finite Subset of SetPrimes st A = {} holds
A -bag = EmptyBag SetPrimes