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 that
A1: p < q and
A2: q <=' r ; :: thesis: p < r
( q < r or q = r ) by A2, Def12;
hence p < r by A1, Th45; :: thesis: verum