let n be Ordinal; :: thesis: LexOrder n is admissible

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 [(EmptyBag n),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 [(EmptyBag n),a] in BagOrder n

let a be bag of n; :: thesis: [(EmptyBag n),a] in BagOrder n
EmptyBag n <=' a by PRE_POLY:60;
hence [(EmptyBag n),a] in BagOrder n by PRE_POLY:def 14; :: thesis: verum

end;

hence for a being bag of n holds [(EmptyBag n),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 A3, PRE_POLY:def 10;

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 A4, A6, XREAL_1:6; :: 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