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

now

assume A4: b1 + b3 = b2 + b4 ; :: thesis: contradiction
( b4 = (b4 + b2) -' b2 & b3 = (b3 + b2) -' b2 ) by POLYNOM1:52;
then A5: b1 + b4 = b2 + b4 by A2, A4, TERMORD:7;
( b1 = (b1 + b4) -' b4 & b2 = (b2 + b4) -' b4 ) by POLYNOM1:52;
hence contradiction by A1, A5, TERMORD:def 3; :: thesis: verum

end;

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