let n be Ordinal; :: thesis: for T being admissible TermOrder of n
for b1, b2, b3 being bag of st b1 < b2,T holds
b1 + b3 < b2 + b3,T
let T be admissible TermOrder of n; :: thesis: for b1, b2, b3 being bag of st b1 < b2,T holds
b1 + b3 < b2 + b3,T
let b1, b2, b3 be bag of ; :: thesis: ( b1 < b2,T implies b1 + b3 < b2 + b3,T )
assume A1: b1 < b2,T ; :: thesis: b1 + b3 < b2 + b3,T
then ( b1 <= b2,T & b1 <> b2 ) by TERMORD:def 3;
then [b1,b2] in T by TERMORD:def 2;
then [(b1 + b3),(b2 + b3)] in T by BAGORDER:def 7;
then A2: b1 + b3 <= b2 + b3,T by TERMORD:def 2;

now

assume A3: b1 + b3 = b2 + b3 ; :: thesis: contradiction
b1 = (b1 + b3) -' b3 by POLYNOM1:52
.= b2 by A3, POLYNOM1:52 ;
hence contradiction by A1, TERMORD:def 3; :: thesis: verum

end;

hence b1 + b3 < b2 + b3,T by A2, TERMORD:def 3; :: thesis: verum