:: deftheorem Def11 defines NaivelyOrderedBags BAGORDER:def 11 :
for n being Nat
for b₂ being strict RelStr holds
( b₂ = NaivelyOrderedBags n iff ( the carrier of b₂ = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b₂ iff x divides y ) ) ) );