ex S being non empty finite Subset of (Bags n) st
( divisors b = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) by Def15;
hence ( not divisors b is empty & divisors b is one-to-one ) ; :: thesis: verum