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 that
A1: x in Bags n and
A2: y in Bags n ; :: thesis: ( [x,y] in InvLexOrder n or [y,x] in InvLexOrder n )
reconsider p = x, q = y as bag of n by A1, A2, PRE_POLY:def 12;

now

assume A3: not [p,q] in InvLexOrder n ; :: thesis: [q,p] in InvLexOrder n
then A4: p <> q by Def8;
set s = SgmX (RelIncl n),((support p) \/ (support q));
A5: dom p = n by PARTFUN1:def 4;
A6: dom q = n by PARTFUN1:def 4;
A7: 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 A8: RelIncl n linearly_orders (support p) \/ (support q) by A7, ORDERS_1:133, ORDERS_1:134;
then A9: rng (SgmX (RelIncl n),((support p) \/ (support q))) = (support p) \/ (support q) by PRE_POLY: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) );
A10: for k being Nat st S₁[k] holds
k <= len (SgmX (RelIncl n),((support p) \/ (support q))) by FINSEQ_3:27;
A11: ex k being Nat st S₁[k]

proof

assume A12: 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 PRE_POLY:def 7;
then x in (support p) \/ (support q) by XBOOLE_0:def 3;
then ex k being Nat st
( k in dom (SgmX (RelIncl n),((support p) \/ (support q))) & (SgmX (RelIncl n),((support p) \/ (support q))) . k = x ) by A9, FINSEQ_2:11;
hence p . x = q . x by A12; :: thesis: verum

end;

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

then x in support q by PRE_POLY:def 7;
then x in (support p) \/ (support q) by XBOOLE_0:def 3;
then ex k being Nat st
( k in dom (SgmX (RelIncl n),((support p) \/ (support q))) & (SgmX (RelIncl n),((support p) \/ (support q))) . k = x ) by A9, FINSEQ_2:11;
hence p . x = q . x by 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 A4, A5, A6, 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(A10, A11);
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 A9;

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 A9, 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 that
A20: not k in support p and
A21: not k in support q ; :: thesis: contradiction
p . k = 0 by A20, PRE_POLY:def 7;
hence contradiction by A19, A21, PRE_POLY:def 7; :: thesis: verum

end;

then k in (support p) \/ (support q) by XBOOLE_0:def 3;
then consider m being Nat such that
A22: m in dom (SgmX (RelIncl n),((support p) \/ (support q))) and
A23: (SgmX (RelIncl n),((support p) \/ (support q))) . m = k by A9, FINSEQ_2:11;
A24: m <= j by A14, A19, A22, A23;
m <> j by A17, A23;
then m < j by A24, XXREAL_0:1;
then [((SgmX (RelIncl n),((support p) \/ (support q))) /. m),((SgmX (RelIncl n),((support p) \/ (support q))) /. j)] in RelIncl n by A8, A13, A22, PRE_POLY:def 2;
then [((SgmX (RelIncl n),((support p) \/ (support q))) . m),((SgmX (RelIncl n),((support p) \/ (support q))) /. j)] in RelIncl n by A22, 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 A9, A15, A18, A23, WELLORD2:def 1;
hence contradiction by A17, A23, ORDINAL1:7; :: thesis: verum

end;

then q . J <= p . J by A3, A9, 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 n holds [(EmptyBag n),a] in InvLexOrder n ) & ( for a, b, c being bag of n st [a,b] in InvLexOrder n holds
[(a + c),(b + c)] in InvLexOrder n ) )

now

let a be bag of n; :: 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 A25: EmptyBag n <> a ; :: thesis: [(EmptyBag n),b₁] in InvLexOrder n

set s = SgmX (RelIncl n),(support a);
A26: 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 A27: RelIncl n linearly_orders support a by A26, ORDERS_1:133, ORDERS_1:134;
then A28: rng (SgmX (RelIncl n),(support a)) = support a by PRE_POLY:def 2;
then rng (SgmX (RelIncl n),(support a)) <> {} by A25, Th20;
then A29: len (SgmX (RelIncl n),(support a)) in dom (SgmX (RelIncl n),(support a)) by FINSEQ_5:6, RELAT_1:60;
then A30: (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 A28;

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 A28, A30; :: thesis: ( (EmptyBag n) . j < a . j & ( for k being Ordinal st j in k & k in n holds
(EmptyBag n) . k = a . k ) )
A31: a . j <> 0 by A28, A30, PRE_POLY:def 7;
(EmptyBag n) . j = 0 by PRE_POLY:52;
hence (EmptyBag n) . j < a . j by A31; :: 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 that
A32: j in k and
A33: k in n ; :: thesis: (EmptyBag n) . k = a . k
A34: j c= k by A32, ORDINAL1:def 2;

now

assume (EmptyBag n) . k <> a . k ; :: thesis: contradiction
then a . k <> 0 by PRE_POLY:52;
then k in support a by PRE_POLY:def 7;
then consider i being Nat such that
A35: i in dom (SgmX (RelIncl n),(support a)) and
A36: (SgmX (RelIncl n),(support a)) . i = k by A28, FINSEQ_2:11;
A37: i <= len (SgmX (RelIncl n),(support a)) by A35, FINSEQ_3:27;

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

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

hence contradiction by A32, A36; :: 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 A27, A29, A35, PRE_POLY:def 2;
then [((SgmX (RelIncl n),(support a)) . i),((SgmX (RelIncl n),(support a)) /. (len (SgmX (RelIncl n),(support a))))] in RelIncl n by A35, 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 A29, PARTFUN1:def 8;
then k c= j by A28, A30, A33, A36, WELLORD2:def 1;
then j = k by A34, XBOOLE_0:def 10;
hence contradiction by A32; :: 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 n holds [(EmptyBag n),a] in InvLexOrder n ; :: thesis: for a, b, c being bag of n st [a,b] in InvLexOrder n holds
[(a + c),(b + c)] in InvLexOrder n

now

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

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

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

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

end;

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

then consider i being Ordinal such that
A40: i in n and
A41: a . i < b . i and
A42: for k being Ordinal st i in k & k in n holds
a . k = b . k by A38, 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 A40; :: 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 ) )
A43: (a + c) . i = (a . i) + (c . i) by PRE_POLY:def 5;
(b + c) . i = (b . i) + (c . i) by PRE_POLY:def 5;
hence (a + c) . i < (b + c) . i by A41, A43, 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 that
A44: i in k and
A45: k in n ; :: thesis: (a + c) . k = (b + c) . k
A46: (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 A42, A44, A45, A46; :: 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 n st [a,b] in InvLexOrder n holds
[(a + c),(b + c)] in InvLexOrder n ; :: thesis: verum