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 A1: ( p < q & q < r ) ; :: thesis: p < r
then consider k being Ordinal such that
A2: p . k < q . k and
A3: for l being Ordinal st l in k holds
p . l = q . l by Def11;
consider m being Ordinal such that
A4: q . m < r . m and
A5: for l being Ordinal st l in m holds
q . l = r . l by A1, Def11;
take n = k /\ m; :: according to POLYNOM1:def 11 :: thesis: ( p . n < r . n & ( for l being Ordinal st l in n holds
p . l = r . l ) )
A6: ( n c= k & n c= m ) by XBOOLE_1:17;
A7: ( ( n c= k & n <> k implies n c< k ) & ( n c< k implies ( n c= k & n <> k ) ) & ( n c= m & n <> m implies n c< m ) & ( n c< m implies ( n c= m & n <> m ) ) ) by XBOOLE_0:def 8;

now

per cases ( k in m or m in k or m = k ) by ORDINAL1:24;

suppose k in m ; :: thesis: p . n < r . n

hence p . n < r . n by A2, A5, A7, ORDINAL1:21, ORDINAL3:16, XBOOLE_1:17; :: thesis: verum

end;

suppose m in k ; :: thesis: p . n < r . n

hence p . n < r . n by A3, A4, A7, ORDINAL1:21, ORDINAL3:16, XBOOLE_1:17; :: thesis: verum

end;

suppose m = k ; :: thesis: p . n < r . n

hence p . n < r . n by A2, A4, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence p . n < r . n ; :: thesis: for l being Ordinal st l in n holds
p . l = r . l
let l be Ordinal; :: thesis: ( l in n implies p . l = r . l )
assume A8: l in n ; :: thesis: p . l = r . l
hence p . l = q . l by A3, A6
.= r . l by A5, A6, A8 ;
:: thesis: verum