let A be finite Subset of SetPrimes; :: thesis: ( A = {} implies A -bag = EmptyBag SetPrimes )
assume A = {} ; :: thesis: A -bag = EmptyBag SetPrimes
then support (A -bag) = {} by BagSupport;
hence A -bag = EmptyBag SetPrimes by PRE_POLY:81; :: thesis: verum