:: deftheorem Def13 defines BagOrder PRE_POLY:def 14 :
for n being Ordinal
for b₂ being Order of (Bags n) holds
( b₂ = BagOrder n iff for p, q being bag of n holds
( [p,q] in b₂ iff p <=' q ) );