let A, B be finite Subset of SetPrimes; :: thesis: ( A -bag = B -bag implies A = B )
assume A -bag = B -bag ; :: thesis: A = B
then A = support (B -bag) by BagSupport;
hence A = B by BagSupport; :: thesis: verum