let n be Ordinal; :: thesis: for b1, b2, b3 being bag of n st b1 <=' b2 holds
b1 + b3 <=' b2 + b3
let b1, b2, b3 be bag of n; :: 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, PRE_POLY:def 10;
then consider k being Ordinal such that
A2: b1 . k < b2 . k and
A3: for l being Ordinal st l in k holds
b1 . l = b2 . l by PRE_POLY:def 9;
A4: now :: thesis: for l being Ordinal st l in k holds
(b1 + b3) . l = (b2 + b3) . l
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 PRE_POLY:def 5
.= (b2 . l) + (b3 . l) by A3, A5
.= (b2 + b3) . l by PRE_POLY:def 5 ; :: thesis: verum
end;
( (b1 + b3) . k = (b1 . k) + (b3 . k) & (b2 + b3) . k = (b2 . k) + (b3 . k) ) by PRE_POLY:def 5;
then (b1 + b3) . k < (b2 + b3) . k by A2, XREAL_1:8;
then b1 + b3 < b2 + b3 by A4, PRE_POLY:def 9;
hence b1 + b3 <=' b2 + b3 by PRE_POLY:def 10; :: thesis: verum
end;
end;