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 )
A1: b3 is Element of Bags n by PRE_POLY:def 12;
field T = Bags n by ORDERS_1:12;
then A2: T is_transitive_in Bags n by RELAT_2:def 16;
assume ( b1 <= b2,T & b2 <= b3,T ) ; :: thesis: b1 <= b3,T
then A3: ( [b1,b2] in T & [b2,b3] in T ) ;
( b1 is Element of Bags n & b2 is Element of Bags n ) by PRE_POLY:def 12;
then [b1,b3] in T by A3, A2, A1, RELAT_2:def 8;
hence b1 <= b3,T ; :: thesis: verum