let n be Ordinal; 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; 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; ( b1 <= b2,T & b2 < b3,T implies b1 < b3,T )
assume that
A1:
b1 <= b2,T
and
A2:
b2 < b3,T
; 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; verum