let n be Ordinal; :: thesis: InvLexOrder n is admissible
set ILO = InvLexOrder n;

now

let x, y be set ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in InvLexOrder n implies [y,x] in InvLexOrder n )
assume A1: ( x in Bags n & y in Bags n ) ; :: thesis: ( [x,y] in InvLexOrder n or [y,x] in InvLexOrder n )
reconsider p = x, q = y as bag of by A1, POLYNOM1:def 14;

now

assume A2: not [p,q] in InvLexOrder n ; :: thesis: [q,p] in InvLexOrder n
then A3: ( p <> q & ( for i being Ordinal holds
( not i in n or not p . i < q . i or ex k being Ordinal st
( i in k & k in n & not p . k = q . k ) ) ) ) by Def8;
set s = SgmX (RelIncl n),((support p) \/ (support q));
A4: ( dom p = n & dom q = n ) by PARTFUN1:def 4;
A5: field (RelIncl n) = n by WELLORD2:def 1;
RelIncl n is well-ordering by WELLORD2:7;
then RelIncl n is being_linear-order by ORDERS_1:107;
then A6: RelIncl n linearly_orders (support p) \/ (support q) by A5, ORDERS_1:133, ORDERS_1:134;
then A7: rng (SgmX (RelIncl n),((support p) \/ (support q))) = (support p) \/ (support q) by TRIANG_1:def 2;
defpred S₁[ Nat] means ( $1 in dom (SgmX (RelIncl n),((support p) \/ (support q))) & q . ((SgmX (RelIncl n),((support p) \/ (support q))) . $1) <> p . ((SgmX (RelIncl n),((support p) \/ (support q))) . $1) );
A8: for k being Nat st S₁[k] holds
k <= len (SgmX (RelIncl n),((support p) \/ (support q))) by FINSEQ_3:27;
A9: ex k being Nat st S₁[k]

proof

assume A10: for k being Nat holds not S₁[k] ; :: thesis: contradiction

now

let x be set ; :: thesis: ( x in n implies p . b₁ = q . b₁ )
assume x in n ; :: thesis: p . b₁ = q . b₁

per cases ( p . x <> 0 or q . x <> 0 or ( p . x = 0 & q . x = 0 ) ) ;

suppose p . x <> 0 ; :: thesis: p . b₁ = q . b₁

then x in support p by POLYNOM1:def 7;
then x in (support p) \/ (support q) by XBOOLE_0:def 3;
then consider k being Nat such that
A11: ( k in dom (SgmX (RelIncl n),((support p) \/ (support q))) & (SgmX (RelIncl n),((support p) \/ (support q))) . k = x ) by A7, FINSEQ_2:11;
thus p . x = q . x by A10, A11; :: thesis: verum

end;

suppose q . x <> 0 ; :: thesis: p . b₁ = q . b₁

then x in support q by POLYNOM1:def 7;
then x in (support p) \/ (support q) by XBOOLE_0:def 3;
then consider k being Nat such that
A12: ( k in dom (SgmX (RelIncl n),((support p) \/ (support q))) & (SgmX (RelIncl n),((support p) \/ (support q))) . k = x ) by A7, FINSEQ_2:11;
thus p . x = q . x by A10, A12; :: thesis: verum

end;

suppose ( p . x = 0 & q . x = 0 ) ; :: thesis: p . b₁ = q . b₁

hence p . x = q . x ; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A4, FUNCT_1:9; :: thesis: verum

end;

consider j being Nat such that
A13: S₁[j] and
A14: for k being Nat st S₁[k] holds
k <= j from NAT_1:sch 6(A8, A9);
A15: (SgmX (RelIncl n),((support p) \/ (support q))) . j in rng (SgmX (RelIncl n),((support p) \/ (support q))) by A13, FUNCT_1:12;
then reconsider J = (SgmX (RelIncl n),((support p) \/ (support q))) . j as Ordinal by A7;

now

take J = J; :: thesis: ( J in n & q . J < p . J & ( for k being Ordinal st J in k & k in n holds
q . k = p . k ) )
thus J in n by A7, A15; :: thesis: ( q . J < p . J & ( for k being Ordinal st J in k & k in n holds
q . k = p . k ) )

A16: now

let k be Ordinal; :: thesis: ( J in k & k in n implies not q . k <> p . k )
assume that
A17: J in k and
A18: k in n and
A19: q . k <> p . k ; :: thesis: contradiction

now

assume ( not k in support p & not k in support q ) ; :: thesis: contradiction
then ( p . k = 0 & q . k = 0 ) by POLYNOM1:def 7;
hence contradiction by A19; :: thesis: verum

end;

then k in (support p) \/ (support q) by XBOOLE_0:def 3;
then consider m being Nat such that
A20: ( m in dom (SgmX (RelIncl n),((support p) \/ (support q))) & (SgmX (RelIncl n),((support p) \/ (support q))) . m = k ) by A7, FINSEQ_2:11;
A21: m <= j by A14, A19, A20;
m <> j by A17, A20;
then m < j by A21, XXREAL_0:1;
then [((SgmX (RelIncl n),((support p) \/ (support q))) /. m),((SgmX (RelIncl n),((support p) \/ (support q))) /. j)] in RelIncl n by A6, A13, A20, TRIANG_1:def 2;
then [((SgmX (RelIncl n),((support p) \/ (support q))) . m),((SgmX (RelIncl n),((support p) \/ (support q))) /. j)] in RelIncl n by A20, PARTFUN1:def 8;
then [((SgmX (RelIncl n),((support p) \/ (support q))) . m),((SgmX (RelIncl n),((support p) \/ (support q))) . j)] in RelIncl n by A13, PARTFUN1:def 8;
then (SgmX (RelIncl n),((support p) \/ (support q))) . m c= (SgmX (RelIncl n),((support p) \/ (support q))) . j by A7, A15, A18, A20, WELLORD2:def 1;
hence contradiction by A17, A20, ORDINAL1:7; :: thesis: verum

end;

then q . J <= p . J by A2, A7, A15, Def8;
hence q . J < p . J by A13, XXREAL_0:1; :: thesis: for k being Ordinal st J in k & k in n holds
q . k = p . k
thus for k being Ordinal st J in k & k in n holds
q . k = p . k by A16; :: thesis: verum

end;

hence [q,p] in InvLexOrder n by Def8; :: thesis: verum

end;

hence ( [x,y] in InvLexOrder n or [y,x] in InvLexOrder n ) ; :: thesis: verum

end;

hence InvLexOrder 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 InvLexOrder n ) & ( for a, b, c being bag of st [a,b] in InvLexOrder n holds
[(a + c),(b + c)] in InvLexOrder n ) )

now

let a be bag of ; :: thesis: [(EmptyBag n),b₁] in InvLexOrder n

per cases ( EmptyBag n = a or EmptyBag n <> a ) ;

suppose EmptyBag n = a ; :: thesis: [(EmptyBag n),b₁] in InvLexOrder n

hence [(EmptyBag n),a] in InvLexOrder n by Def8; :: thesis: verum

end;

suppose A22: EmptyBag n <> a ; :: thesis: [(EmptyBag n),b₁] in InvLexOrder n

set s = SgmX (RelIncl n),(support a);
A23: field (RelIncl n) = n by WELLORD2:def 1;
RelIncl n is well-ordering by WELLORD2:7;
then RelIncl n is being_linear-order by ORDERS_1:107;
then A24: RelIncl n linearly_orders support a by A23, ORDERS_1:133, ORDERS_1:134;
then A25: rng (SgmX (RelIncl n),(support a)) = support a by TRIANG_1:def 2;
then rng (SgmX (RelIncl n),(support a)) <> {} by A22, Th20;
then A26: len (SgmX (RelIncl n),(support a)) in dom (SgmX (RelIncl n),(support a)) by FINSEQ_5:6, RELAT_1:60;
then A27: (SgmX (RelIncl n),(support a)) . (len (SgmX (RelIncl n),(support a))) in rng (SgmX (RelIncl n),(support a)) by FUNCT_1:12;
then reconsider j = (SgmX (RelIncl n),(support a)) . (len (SgmX (RelIncl n),(support a))) as Ordinal by A25;

now

take j = j; :: thesis: ( j in n & (EmptyBag n) . j < a . j & ( for k being Ordinal st j in k & k in n holds
(EmptyBag n) . k = a . k ) )
thus j in n by A25, A27; :: thesis: ( (EmptyBag n) . j < a . j & ( for k being Ordinal st j in k & k in n holds
(EmptyBag n) . k = a . k ) )
A28: a . j <> 0 by A25, A27, POLYNOM1:def 7;
(EmptyBag n) . j = 0 by POLYNOM1:56;
hence (EmptyBag n) . j < a . j by A28; :: thesis: for k being Ordinal st j in k & k in n holds
(EmptyBag n) . k = a . k
let k be Ordinal; :: thesis: ( j in k & k in n implies (EmptyBag n) . k = a . k )
assume A29: ( j in k & k in n ) ; :: thesis: (EmptyBag n) . k = a . k
A30: j c= k by A29, ORDINAL1:def 2;

now

assume (EmptyBag n) . k <> a . k ; :: thesis: contradiction
then a . k <> 0 by POLYNOM1:56;
then k in support a by POLYNOM1:def 7;
then consider i being Nat such that
A31: ( i in dom (SgmX (RelIncl n),(support a)) & (SgmX (RelIncl n),(support a)) . i = k ) by A25, FINSEQ_2:11;
A32: i <= len (SgmX (RelIncl n),(support a)) by A31, FINSEQ_3:27;

per cases ( i = len (SgmX (RelIncl n),(support a)) or i < len (SgmX (RelIncl n),(support a)) ) by A32, XXREAL_0:1;

suppose i = len (SgmX (RelIncl n),(support a)) ; :: thesis: contradiction

hence contradiction by A29, A31; :: thesis: verum

end;

suppose i < len (SgmX (RelIncl n),(support a)) ; :: thesis: contradiction

then [((SgmX (RelIncl n),(support a)) /. i),((SgmX (RelIncl n),(support a)) /. (len (SgmX (RelIncl n),(support a))))] in RelIncl n by A24, A26, A31, TRIANG_1:def 2;
then [((SgmX (RelIncl n),(support a)) . i),((SgmX (RelIncl n),(support a)) /. (len (SgmX (RelIncl n),(support a))))] in RelIncl n by A31, PARTFUN1:def 8;
then [((SgmX (RelIncl n),(support a)) . i),((SgmX (RelIncl n),(support a)) . (len (SgmX (RelIncl n),(support a))))] in RelIncl n by A26, PARTFUN1:def 8;
then k c= j by A25, A27, A29, A31, WELLORD2:def 1;
then j = k by A30, XBOOLE_0:def 10;
hence contradiction by A29; :: thesis: verum

end;

end;

end;

hence (EmptyBag n) . k = a . k ; :: thesis: verum

end;

hence [(EmptyBag n),a] in InvLexOrder n by Def8; :: thesis: verum

end;

end;

end;

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

now

let a, b, c be bag of ; :: thesis: ( [a,b] in InvLexOrder n implies [(b₁ + b₃),(b₂ + b₃)] in InvLexOrder n )
assume A33: [a,b] in InvLexOrder n ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in InvLexOrder n

per cases ( a = b or a <> b ) ;

suppose A34: a = b ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in InvLexOrder n

a + c in Bags n by POLYNOM1:def 14;
hence [(a + c),(b + c)] in InvLexOrder n by A34, ORDERS_1:12; :: thesis: verum

end;

suppose a <> b ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in InvLexOrder n

then consider i being Ordinal such that
A35: ( i in n & a . i < b . i ) and
A36: for k being Ordinal st i in k & k in n holds
a . k = b . k by A33, Def8;

now

take i = i; :: thesis: ( i in n & (a + c) . i < (b + c) . i & ( for k being Ordinal st i in k & k in n holds
(a + c) . k = (b + c) . k ) )
thus i in n by A35; :: thesis: ( (a + c) . i < (b + c) . i & ( for k being Ordinal st i in k & k in n holds
(a + c) . k = (b + c) . k ) )
( (a + c) . i = (a . i) + (c . i) & (b + c) . i = (b . i) + (c . i) ) by POLYNOM1:def 5;
hence (a + c) . i < (b + c) . i by A35, XREAL_1:8; :: thesis: for k being Ordinal st i in k & k in n holds
(a + c) . k = (b + c) . k
let k be Ordinal; :: thesis: ( i in k & k in n implies (a + c) . k = (b + c) . k )
assume A37: ( i in k & k in n ) ; :: thesis: (a + c) . k = (b + c) . k
( (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 A36, A37; :: thesis: verum

end;

hence [(a + c),(b + c)] in InvLexOrder n by Def8; :: thesis: verum

end;

end;

end;

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