let n be Ordinal; :: thesis:
now :: thesis: for a, b being object st a in Bags n & b in Bags n & not [a,b] in BagOrder n holds
[b,a] in BagOrder n
let a, b be object ; :: thesis: ( a in Bags n & b in Bags n & not [a,b] in BagOrder n implies [b,a] in BagOrder n )
assume that
A1: a in Bags n and
A2: b in Bags n ; :: thesis: ( [a,b] in BagOrder n or [b,a] in BagOrder n )
reconsider a9 = a, b9 = b as bag of n by A1, A2;
( a9 <=' b9 or b9 <=' a9 ) by PRE_POLY:45;
hence ( [a,b] in BagOrder n or [b,a] in BagOrder n ) by PRE_POLY:def 14; :: thesis: verum
end;
hence LexOrder n is_strongly_connected_in Bags n ; :: according to BAGORDER:def 5 :: thesis: ( ( for a being bag of n holds [(),a] in LexOrder n ) & ( for a, b, c being bag of n st [a,b] in LexOrder n holds
[(a + c),(b + c)] in LexOrder n ) )

now :: thesis: for a being bag of n holds [(),a] in BagOrder nend;
hence for a being bag of n holds [(),a] in LexOrder n ; :: thesis: for a, b, c being bag of n st [a,b] in LexOrder n holds
[(a + c),(b + c)] in LexOrder n

now :: thesis: for a, b, c being bag of n st [a,b] in BagOrder n holds
[(a + c),(b + c)] in BagOrder n
let a, b, c be bag of n; :: thesis: ( [a,b] in BagOrder n implies [(a + c),(b + c)] in BagOrder n )
assume [a,b] in BagOrder n ; :: thesis: [(a + c),(b + c)] in BagOrder n
then A3: a <=' b by PRE_POLY:def 14;
now :: thesis: a + c <=' b + c
per cases ( a < b or a = b ) by ;
suppose a < b ; :: thesis: a + c <=' b + c
then consider k being Ordinal such that
A4: a . k < b . k and
A5: for l being Ordinal st l in k holds
a . l = b . l by PRE_POLY:def 9;
now :: thesis: ex k being Ordinal st
( (a + c) . k < (b + c) . k & ( for l being Ordinal st l in k holds
(a + c) . l = (b + c) . l ) )
take k = k; :: thesis: ( (a + c) . k < (b + c) . k & ( for l being Ordinal st l in k holds
(a + c) . l = (b + c) . l ) )

A6: (a + c) . k = (a . k) + (c . k) by PRE_POLY:def 5;
(b + c) . k = (b . k) + (c . k) by PRE_POLY:def 5;
hence (a + c) . k < (b + c) . k by ; :: thesis: for l being Ordinal st l in k holds
(a + c) . l = (b + c) . l

let l be Ordinal; :: thesis: ( l in k implies (a + c) . l = (b + c) . l )
assume A7: l in k ; :: thesis: (a + c) . l = (b + c) . l
A8: (a + c) . l = (a . l) + (c . l) by PRE_POLY:def 5;
(b + c) . l = (b . l) + (c . l) by PRE_POLY:def 5;
hence (a + c) . l = (b + c) . l by A5, A7, A8; :: thesis: verum
end;
then a + c < b + c by PRE_POLY:def 9;
hence a + c <=' b + c by PRE_POLY:def 10; :: thesis: verum
end;
suppose a = b ; :: thesis: a + c <=' b + c
hence a + c <=' b + c ; :: thesis: verum
end;
end;
end;
hence [(a + c),(b + c)] in BagOrder n by PRE_POLY:def 14; :: thesis: verum
end;
hence for a, b, c being bag of n st [a,b] in LexOrder n holds
[(a + c),(b + c)] in LexOrder n ; :: thesis: verum