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

[(a + c),(b + c)] in LexOrder n ) )

[(a + c),(b + c)] in LexOrder n

[(a + c),(b + c)] in LexOrder n ; :: thesis: verum

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

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 [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;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

[(a + c),(b + c)] in LexOrder n ) )

now :: thesis: for a being bag of n holds [(EmptyBag n),a] in BagOrder n

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 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;EmptyBag n <=' a by PRE_POLY:60;

hence [(EmptyBag n),a] in BagOrder n by PRE_POLY:def 14; :: thesis: verum

[(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

hence
for a, b, c being bag of n st [a,b] in LexOrder 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;

end;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 + cend;

hence
[(a + c),(b + c)] in BagOrder n
by PRE_POLY:def 14; :: thesis: verumper cases
( a < b or a = b )
by A3, PRE_POLY:def 10;

end;

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;

hence a + c <=' b + c by PRE_POLY:def 10; :: thesis: verum

end;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 ) )

then
a + c < b + c
by PRE_POLY:def 9;( (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;(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

hence a + c <=' b + c by PRE_POLY:def 10; :: thesis: verum

[(a + c),(b + c)] in LexOrder n ; :: thesis: verum