:: deftheorem Def15 defines divisors PRE_POLY:def 16 :
for n being Ordinal
for b being bag of n
for b₃ being FinSequence of Bags n holds
( b₃ = divisors b iff ex S being non empty finite Subset of (Bags n) st
( b₃ = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) );