:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
for n being Ordinal
for b₂ being Order of (Bags n) holds
( b₂ = DivOrder n iff for b1, b2 being bag of n holds
( [b1,b2] in b₂ iff b1 divides b2 ) );