let n be Ordinal; :: thesis: BagOrder n is_transitive_in Bags n
set BO = BagOrder n;
let x, y, z be object ; :: 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 and
A2: y in Bags n and
A3: z in Bags n and
A4: ( [x,y] in BagOrder n & [y,z] in BagOrder n ) ; :: thesis: [x,z] in BagOrder n
reconsider b19 = y, b29 = z as bag of n by A2, A3;
reconsider b1 = x, b2 = y as bag of n by A1, A2;
reconsider B1 = b1, B29 = b29 as bag of n ;
( b1 <=' b2 & b19 <=' b29 ) by A4, Def13;
then B1 <=' B29 by Th41;
hence [x,z] in BagOrder n by Def13; :: thesis: verum