let n be Ordinal; :: thesis: for T being admissible TermOrder of n

for b1, b2, b3 being bag of n 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 n st b1 <= b2,T holds

b1 + b3 <= b2 + b3,T

let b1, b2, b3 be bag of n; :: thesis: ( b1 <= b2,T implies b1 + b3 <= b2 + b3,T )

assume b1 <= b2,T ; :: thesis: b1 + b3 <= b2 + b3,T

then [b1,b2] in T by TERMORD:def 2;

then [(b1 + b3),(b2 + b3)] in T by BAGORDER:def 5;

hence b1 + b3 <= b2 + b3,T by TERMORD:def 2; :: thesis: verum

for b1, b2, b3 being bag of n 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 n st b1 <= b2,T holds

b1 + b3 <= b2 + b3,T

let b1, b2, b3 be bag of n; :: thesis: ( b1 <= b2,T implies b1 + b3 <= b2 + b3,T )

assume b1 <= b2,T ; :: thesis: b1 + b3 <= b2 + b3,T

then [b1,b2] in T by TERMORD:def 2;

then [(b1 + b3),(b2 + b3)] in T by BAGORDER:def 5;

hence b1 + b3 <= b2 + b3,T by TERMORD:def 2; :: thesis: verum