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

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

b1 + b3 < b2 + b4,T

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

assume that

A1: b1 < b2,T and

A2: b3 <= b4,T ; :: thesis: b1 + b3 < b2 + b4,T

b1 <= b2,T by A1, TERMORD:def 3;

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

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

then A3: b1 + b3 <= b2 + b3,T by TERMORD:def 2;

[b3,b4] in T by A2, TERMORD:def 2;

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

then A4: b2 + b3 <= b2 + b4,T by TERMORD:def 2;

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

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

b1 + b3 < b2 + b4,T

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

assume that

A1: b1 < b2,T and

A2: b3 <= b4,T ; :: thesis: b1 + b3 < b2 + b4,T

b1 <= b2,T by A1, TERMORD:def 3;

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

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

then A3: b1 + b3 <= b2 + b3,T by TERMORD:def 2;

[b3,b4] in T by A2, TERMORD:def 2;

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

then A4: b2 + b3 <= b2 + b4,T by TERMORD:def 2;

A5: now :: thesis: not b1 + b3 = b2 + b4

b1 + b3 <= b2 + b4,T
by A3, A4, TERMORD:8;A6:
( b1 = (b1 + b4) -' b4 & b2 = (b2 + b4) -' b4 )
by PRE_POLY:48;

A7: ( b4 = (b4 + b2) -' b2 & b3 = (b3 + b2) -' b2 ) by PRE_POLY:48;

assume b1 + b3 = b2 + b4 ; :: thesis: contradiction

then b1 + b4 = b2 + b4 by A3, A4, A7, TERMORD:7;

hence contradiction by A1, A6, TERMORD:def 3; :: thesis: verum

end;A7: ( b4 = (b4 + b2) -' b2 & b3 = (b3 + b2) -' b2 ) by PRE_POLY:48;

assume b1 + b3 = b2 + b4 ; :: thesis: contradiction

then b1 + b4 = b2 + b4 by A3, A4, A7, TERMORD:7;

hence contradiction by A1, A6, TERMORD:def 3; :: thesis: verum

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