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
( q < r or q = r ) by A2, Def10;
hence p < r by A1, Th41; :: thesis: verum