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