let n be Ordinal; 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; 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; ( b1 < b2,T & b3 <= b4,T implies b1 + b3 < b2 + b4,T )
assume that
A1:
b1 < b2,T
and
A2:
b3 <= b4,T
; 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 not b1 + b3 = b2 + b4end;
b1 + b3 <= b2 + b4,T
by A3, A4, TERMORD:8;
hence
b1 + b3 < b2 + b4,T
by A5, TERMORD:def 3; verum