for n being Ordinal
for T being admissible TermOrder of n
for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T