let n be Ordinal; :: thesis: for p, q, r being bag of st p <=' q & q <=' r holds
p <=' r
let p, q, r be bag of ; :: thesis: ( p <=' q & q <=' r implies p <=' r )
assume ( p <=' q & q <=' r ) ; :: thesis: p <=' r
then ( ( p < q or p = q ) & ( q < r or q = r ) ) by Def12;
then ( p < r or p <=' r ) by Th45;
hence p <=' r by Def12; :: thesis: verum