let n be Ordinal; :: thesis: for T being TermOrder of n
for b1, b2, b3 being bag of 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 st b1 <= b2,T & b2 < b3,T holds
b1 < b3,T
let b1, b2, b3 be bag of ; :: thesis: ( b1 <= b2,T & b2 < b3,T implies b1 < b3,T )
assume A1: ( b1 <= b2,T & b2 < b3,T ) ; :: thesis: b1 < b3,T
then A2: ( b2 <= b3,T & b2 <> b3 ) by TERMORD:def 3;
then A3: b1 <= b3,T by A1, TERMORD:8;
b1 <> b3 by A1, A2, TERMORD:7;
hence b1 < b3,T by A3, TERMORD:def 3; :: thesis: verum