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
consider k being Ordinal such that
A3: p . k < q . k and
A4: for l being Ordinal st l in k holds
p . l = q . l by A1;
consider m being Ordinal such that
A5: q . m < r . m and
A6: for l being Ordinal st l in m holds
q . l = r . l by A2;
take n = k /\ m; :: according to PRE_POLY:def 9 :: thesis: ( p . n < r . n & ( for l being Ordinal st l in n holds
p . l = r . l ) )
A7: ( ( n c= m & n <> m ) iff n c< m ) ;
A8: ( ( n c= k & n <> k ) iff n c< k ) ;

now :: thesis: p . n < r . n

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

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

hence p . n < r . n by A3, A6, A8, A7, ORDINAL1:11, ORDINAL3:13, XBOOLE_1:17; :: thesis: verum

end;

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

hence p . n < r . n by A4, A5, A8, A7, ORDINAL1:11, ORDINAL3:13, XBOOLE_1:17; :: thesis: verum

end;

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

hence p . n < r . n by A3, A5, 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 )
A9: n c= m by XBOOLE_1:17;
assume A10: l in n ; :: thesis: p . l = r . l
n c= k by XBOOLE_1:17;
hence p . l = q . l by A4, A10
.= r . l by A6, A9, A10 ;
:: thesis: verum