:: deftheorem DO defines DivOrder BAGORD_2:def 6 :
for I being set
for b₂ being Relation of (Bags I) holds
( b₂ = DivOrder I iff for b1, b2 being bag of I holds
( [b1,b2] in b₂ iff ( b1 <> b2 & b1 divides b2 ) ) );