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

now

let a, b be set ; :: thesis: ( a in Bags n & b in Bags n & not [a,b] in BagOrder n implies [b,a] in BagOrder n )
assume A1: ( a in Bags n & b in Bags n ) ; :: thesis: ( [a,b] in BagOrder n or [b,a] in BagOrder n )
reconsider a' = a, b' = b as bag of by A1, POLYNOM1:def 14;
( a' <=' b' or b' <=' a' ) by POLYNOM1:49;
hence ( [a,b] in BagOrder n or [b,a] in BagOrder n ) by POLYNOM1:def 16; :: thesis: verum

end;

hence LexOrder n is_strongly_connected_in Bags n by RELAT_2:def 7; :: according to BAGORDER:def 7 :: thesis: ( ( for a being bag of holds [(EmptyBag n),a] in LexOrder n ) & ( for a, b, c being bag of st [a,b] in LexOrder n holds
[(a + c),(b + c)] in LexOrder n ) )

now

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

end;

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

now

let a, b, c be bag of ; :: thesis: ( [a,b] in BagOrder n implies [(a + c),(b + c)] in BagOrder n )
assume A2: [a,b] in BagOrder n ; :: thesis: [(a + c),(b + c)] in BagOrder n
A3: a <=' b by A2, POLYNOM1:def 16;

now

per cases ( a < b or a = b ) by A3, POLYNOM1:def 12;

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 POLYNOM1:def 11;

now

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 ) )
( (a + c) . k = (a . k) + (c . k) & (b + c) . k = (b . k) + (c . k) ) by POLYNOM1:def 5;
hence (a + c) . k < (b + c) . k by A4, XREAL_1:8; :: 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 A6: l in k ; :: thesis: (a + c) . l = (b + c) . l
( (a + c) . l = (a . l) + (c . l) & (b + c) . l = (b . l) + (c . l) ) by POLYNOM1:def 5;
hence (a + c) . l = (b + c) . l by A5, A6; :: thesis: verum

end;

then a + c < b + c by POLYNOM1:def 11;
hence a + c <=' b + c by POLYNOM1:def 12; :: 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 POLYNOM1:def 16; :: thesis: verum

end;

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