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