let n be Ordinal; :: thesis: for T being admissible TermOrder of n
for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
let T be admissible TermOrder of n; :: thesis: for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
let b1, b2 be bag of n; :: thesis: ( b1 divides b2 implies b1 <= b2,T )
assume b1 divides b2 ; :: thesis: b1 <= b2,T
then consider b3 being bag of n such that
A1: b2 = b1 + b3 by Th1;
EmptyBag n <= b3,T by Th9;
then [(EmptyBag n),b3] in T ;
then [((EmptyBag n) + b1),b2] in T by A1, BAGORDER:def 5;
then [b1,b2] in T by PRE_POLY:53;
hence b1 <= b2,T ; :: thesis: verum