let n be Ordinal; :: thesis: for p, q, r being bag of n st p <=' q & q <=' r holds
p <=' r
let p, q, r be bag of n; :: thesis: ( p <=' q & q <=' r implies p <=' r )
assume that
A1: p <=' q and
A2: q <=' r ; :: thesis: p <=' r
A3: ( q < r or q = r ) by A2, Def10;
( p < q or p = q ) by A1, Def10;
then ( p < r or p <=' r ) by A3, Th41;
hence p <=' r by Def10; :: thesis: verum