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

set ILO = InvLexOrder n;

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

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

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

set ILO = InvLexOrder n;

now :: thesis: for x, y being object st x in Bags n & y in Bags n & not [x,y] in InvLexOrder n holds

[y,x] in InvLexOrder n

hence
InvLexOrder n is_strongly_connected_in Bags n
; :: according to BAGORDER:def 5 :: 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 [y,x] in InvLexOrder n

let x, y be object ; :: 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;

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

now :: thesis: ( not [p,q] in InvLexOrder n implies [q,p] in InvLexOrder n )

hence
( [x,y] in InvLexOrder n or [y,x] in InvLexOrder n )
; :: thesis: verumassume A3:
not [p,q] in InvLexOrder n
; :: thesis: [q,p] in InvLexOrder n

then A4: p <> q by Def6;

set s = SgmX ((RelIncl n),((support p) \/ (support q)));

A5: dom p = n by PARTFUN1:def 2;

A6: dom q = n by PARTFUN1:def 2;

A7: field (RelIncl n) = n by WELLORD2:def 1;

RelIncl n is being_linear-order by ORDERS_1:19;

then A8: RelIncl n linearly_orders (support p) \/ (support q) by A7, ORDERS_1:37, ORDERS_1:38;

then A9: rng (SgmX ((RelIncl n),((support p) \/ (support q)))) = (support p) \/ (support q) by PRE_POLY:def 2;

defpred S_{1}[ 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_{1}[k] holds

k <= len (SgmX ((RelIncl n),((support p) \/ (support q)))) by FINSEQ_3:25;

A11: ex k being Nat st S_{1}[k]

A13: S_{1}[j]
and

A14: for k being Nat st S_{1}[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:3;

then reconsider J = (SgmX ((RelIncl n),((support p) \/ (support q)))) . j as Ordinal by A9;

end;then A4: p <> q by Def6;

set s = SgmX ((RelIncl n),((support p) \/ (support q)));

A5: dom p = n by PARTFUN1:def 2;

A6: dom q = n by PARTFUN1:def 2;

A7: field (RelIncl n) = n by WELLORD2:def 1;

RelIncl n is being_linear-order by ORDERS_1:19;

then A8: RelIncl n linearly_orders (support p) \/ (support q) by A7, ORDERS_1:37, ORDERS_1:38;

then A9: rng (SgmX ((RelIncl n),((support p) \/ (support q)))) = (support p) \/ (support q) by PRE_POLY:def 2;

defpred S

A10: for k being Nat st S

k <= len (SgmX ((RelIncl n),((support p) \/ (support q)))) by FINSEQ_3:25;

A11: ex k being Nat st S

proof

consider j being Nat such that
assume A12:
for k being Nat holds not S_{1}[k]
; :: thesis: contradiction

end;now :: thesis: for x being object st x in n holds

p . x = q . x

hence
contradiction
by A4, A5, A6, FUNCT_1:2; :: thesis: verump . x = q . x

let x be object ; :: thesis: ( x in n implies p . b_{1} = q . b_{1} )

assume x in n ; :: thesis: p . b_{1} = q . b_{1}

end;assume x in n ; :: thesis: p . b

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

end;

suppose
p . x <> 0
; :: thesis: p . b_{1} = q . b_{1}

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:10;

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

end;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:10;

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

suppose
q . x <> 0
; :: thesis: p . b_{1} = q . b_{1}

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:10;

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

end;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:10;

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

A13: S

A14: for k being Nat st S

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:3;

then reconsider J = (SgmX ((RelIncl n),((support p) \/ (support q)))) . j as Ordinal by A9;

now :: thesis: ex J being Ordinal st

( J in n & q . J < p . J & ( for k being Ordinal st J in k & k in n holds

q . k = p . k ) )

hence
[q,p] in InvLexOrder n
by Def6; :: thesis: verum( J in n & q . J < p . J & ( for k being Ordinal st J in k & k in n holds

q . k = p . k ) )

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

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;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 :: thesis: for k being Ordinal st J in k & k in n holds

not q . k <> p . k

then
q . J <= p . J
by A3, A9, A15, Def6;not q . k <> p . k

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

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:10;

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

then [((SgmX ((RelIncl n),((support p) \/ (support q)))) . m),((SgmX ((RelIncl n),((support p) \/ (support q)))) . j)] in RelIncl n by A13, PARTFUN1:def 6;

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:5; :: thesis: verum

end;assume that

A17: J in k and

A18: k in n and

A19: q . k <> p . k ; :: thesis: contradiction

now :: thesis: ( not k in support p implies k in support q )

then
k in (support p) \/ (support q)
by XBOOLE_0:def 3;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;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

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:10;

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

then [((SgmX ((RelIncl n),((support p) \/ (support q)))) . m),((SgmX ((RelIncl n),((support p) \/ (support q)))) . j)] in RelIncl n by A13, PARTFUN1:def 6;

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:5; :: thesis: verum

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

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

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

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 let a be bag of n; :: thesis: [(EmptyBag n),b_{1}] in InvLexOrder n

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

end;

suppose A25:
EmptyBag n <> a
; :: thesis: [(EmptyBag n),b_{1}] in InvLexOrder n

set s = SgmX ((RelIncl n),(support a));

A26: field (RelIncl n) = n by WELLORD2:def 1;

RelIncl n is being_linear-order by ORDERS_1:19;

then A27: RelIncl n linearly_orders support a by A26, ORDERS_1:37, ORDERS_1:38;

then A28: rng (SgmX ((RelIncl n),(support a))) = support a by PRE_POLY:def 2;

then rng (SgmX ((RelIncl n),(support a))) <> {} by A25, PRE_POLY:81;

then A29: len (SgmX ((RelIncl n),(support a))) in dom (SgmX ((RelIncl n),(support a))) by FINSEQ_5:6, RELAT_1:38;

then A30: (SgmX ((RelIncl n),(support a))) . (len (SgmX ((RelIncl n),(support a)))) in rng (SgmX ((RelIncl n),(support a))) by FUNCT_1:3;

then reconsider j = (SgmX ((RelIncl n),(support a))) . (len (SgmX ((RelIncl n),(support a)))) as Ordinal by A28;

end;A26: field (RelIncl n) = n by WELLORD2:def 1;

RelIncl n is being_linear-order by ORDERS_1:19;

then A27: RelIncl n linearly_orders support a by A26, ORDERS_1:37, ORDERS_1:38;

then A28: rng (SgmX ((RelIncl n),(support a))) = support a by PRE_POLY:def 2;

then rng (SgmX ((RelIncl n),(support a))) <> {} by A25, PRE_POLY:81;

then A29: len (SgmX ((RelIncl n),(support a))) in dom (SgmX ((RelIncl n),(support a))) by FINSEQ_5:6, RELAT_1:38;

then A30: (SgmX ((RelIncl n),(support a))) . (len (SgmX ((RelIncl n),(support a)))) in rng (SgmX ((RelIncl n),(support a))) by FUNCT_1:3;

then reconsider j = (SgmX ((RelIncl n),(support a))) . (len (SgmX ((RelIncl n),(support a)))) as Ordinal by A28;

now :: thesis: ex j being Ordinal st

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

hence
[(EmptyBag n),a] in InvLexOrder n
by Def6; :: thesis: verum( 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 ) )

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 PBOOLE:5;

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;

end;(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 PBOOLE:5;

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 :: thesis: not (EmptyBag n) . k <> a . k

hence
(EmptyBag n) . k = a . k
; :: thesis: verumassume
(EmptyBag n) . k <> a . k
; :: thesis: contradiction

then a . k <> 0 by PBOOLE:5;

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:10;

A37: i <= len (SgmX ((RelIncl n),(support a))) by A35, FINSEQ_3:25;

end;then a . k <> 0 by PBOOLE:5;

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:10;

A37: i <= len (SgmX ((RelIncl n),(support a))) by A35, FINSEQ_3:25;

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

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

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

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

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

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

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

now :: thesis: for a, b, c being bag of n st [a,b] in InvLexOrder n holds

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

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

let a, b, c be bag of n; :: thesis: ( [a,b] in InvLexOrder n implies [(b_{1} + b_{3}),(b_{2} + b_{3})] in InvLexOrder n )

assume A38: [a,b] in InvLexOrder n ; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] in InvLexOrder n

end;assume A38: [a,b] in InvLexOrder n ; :: thesis: [(b

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

end;

suppose A39:
a = b
; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] 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:3; :: thesis: verum

end;hence [(a + c),(b + c)] in InvLexOrder n by A39, ORDERS_1:3; :: thesis: verum

suppose
a <> b
; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] 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, Def6;

end;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, Def6;

now :: thesis: ex i being Ordinal st

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

hence
[(a + c),(b + c)] in InvLexOrder n
by Def6; :: thesis: verum( 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 ) )

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:6; :: 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;(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:6; :: 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

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