let n be Ordinal; :: thesis: BagOrder n is_transitive_in Bags n
set BO = BagOrder n;
let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in Bags n or not y in Bags n or not z in Bags n or not [x,y] in BagOrder n or not [y,z] in BagOrder n or [x,z] in BagOrder n )
assume that
A1: ( x in Bags n & y in Bags n & z in Bags n ) and
A2: ( [x,y] in BagOrder n & [y,z] in BagOrder n ) ; :: thesis: [x,z] in BagOrder n
reconsider b1 = x, b2 = y as bag of by A1, Def14;
A3: b1 <=' b2 by A2, Def16;
reconsider b1' = y, b2' = z as bag of by A1, Def14;
A4: b1' <=' b2' by A2, Def16;
reconsider B1 = b1, B2' = b2' as bag of ;
B1 <=' B2' by A3, A4, Th46;
hence [x,z] in BagOrder n by Def16; :: thesis: verum