let n be Ordinal; :: thesis: for b1, b2, b3 being bag of st b1 <=' b2 holds
b1 + b3 <=' b2 + b3
let b1, b2, b3 be bag of ; :: thesis: ( b1 <=' b2 implies b1 + b3 <=' b2 + b3 )
assume A1: b1 <=' b2 ; :: thesis: b1 + b3 <=' b2 + b3

per cases ( b1 = b2 or b1 <> b2 ) ;

suppose b1 = b2 ; :: thesis: b1 + b3 <=' b2 + b3

hence b1 + b3 <=' b2 + b3 ; :: thesis: verum

end;

suppose b1 <> b2 ; :: thesis: b1 + b3 <=' b2 + b3

then b1 < b2 by A1, POLYNOM1:def 12;
then consider k being Ordinal such that
A2: ( b1 . k < b2 . k & ( for l being Ordinal st l in k holds
b1 . l = b2 . l ) ) by POLYNOM1:def 11;
A3: (b1 + b3) . k = (b1 . k) + (b3 . k) by POLYNOM1:def 5;
(b2 + b3) . k = (b2 . k) + (b3 . k) by POLYNOM1:def 5;
then A4: (b1 + b3) . k < (b2 + b3) . k by A2, A3, XREAL_1:10;

now

let l be Ordinal; :: thesis: ( l in k implies (b1 + b3) . l = (b2 + b3) . l )
assume A5: l in k ; :: thesis: (b1 + b3) . l = (b2 + b3) . l
thus (b1 + b3) . l = (b1 . l) + (b3 . l) by POLYNOM1:def 5
.= (b2 . l) + (b3 . l) by A2, A5
.= (b2 + b3) . l by POLYNOM1:def 5 ; :: thesis: verum

end;

then b1 + b3 < b2 + b3 by A4, POLYNOM1:def 11;
hence b1 + b3 <=' b2 + b3 by POLYNOM1:def 12; :: thesis: verum

end;

end;