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

for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

let T be TermOrder of n; :: thesis: for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

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

assume that

A1: b1 <= b2,T and

A2: b2 < b3,T ; :: thesis: b1 < b3,T

A3: b2 <= b3,T by A2, TERMORD:def 3;

then A4: b1 <= b3,T by A1, TERMORD:8;

b2 <> b3 by A2, TERMORD:def 3;

then b1 <> b3 by A1, A3, TERMORD:7;

hence b1 < b3,T by A4, TERMORD:def 3; :: thesis: verum

for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

let T be TermOrder of n; :: thesis: for b1, b2, b3 being bag of n st b1 <= b2,T & b2 < b3,T holds

b1 < b3,T

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

assume that

A1: b1 <= b2,T and

A2: b2 < b3,T ; :: thesis: b1 < b3,T

A3: b2 <= b3,T by A2, TERMORD:def 3;

then A4: b1 <= b3,T by A1, TERMORD:8;

b2 <> b3 by A2, TERMORD:def 3;

then b1 <> b3 by A1, A3, TERMORD:7;

hence b1 < b3,T by A4, TERMORD:def 3; :: thesis: verum