let n be Ordinal; :: thesis:
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
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;
now :: thesis: ( not [p,q] in InvLexOrder n implies [q,p] in InvLexOrder n )
assume A3: not [p,q] in InvLexOrder n ; :: thesis: [q,p] in InvLexOrder n
then A4: p <> q by Def6;
set s = SgmX ((),(() \/ ()));
A5: dom p = n by PARTFUN1:def 2;
A6: dom q = n by PARTFUN1:def 2;
A7: field () = n by WELLORD2:def 1;
RelIncl n is being_linear-order by ORDERS_1:19;
then A8: RelIncl n linearly_orders () \/ () by ;
then A9: rng (SgmX ((),(() \/ ()))) = () \/ () by PRE_POLY:def 2;
defpred S1[ Nat] means ( \$1 in dom (SgmX ((),(() \/ ()))) & q . ((SgmX ((),(() \/ ()))) . \$1) <> p . ((SgmX ((),(() \/ ()))) . \$1) );
A10: for k being Nat st S1[k] holds
k <= len (SgmX ((),(() \/ ()))) by FINSEQ_3:25;
A11: ex k being Nat st S1[k]
proof
assume A12: for k being Nat holds not S1[k] ; :: thesis: contradiction
now :: thesis: for x being object st x in n holds
p . x = q . x
let x be object ; :: thesis: ( x in n implies p . b1 = q . b1 )
assume x in n ; :: thesis: p . b1 = q . b1
per cases ( p . x <> 0 or q . x <> 0 or ( p . x = 0 & q . x = 0 ) ) ;
suppose p . x <> 0 ; :: thesis: p . b1 = q . b1
then x in support p by PRE_POLY:def 7;
then x in () \/ () by XBOOLE_0:def 3;
then ex k being Nat st
( k in dom (SgmX ((),(() \/ ()))) & (SgmX ((),(() \/ ()))) . k = x ) by ;
hence p . x = q . x by A12; :: thesis: verum
end;
suppose q . x <> 0 ; :: thesis: p . b1 = q . b1
then x in support q by PRE_POLY:def 7;
then x in () \/ () by XBOOLE_0:def 3;
then ex k being Nat st
( k in dom (SgmX ((),(() \/ ()))) & (SgmX ((),(() \/ ()))) . k = x ) by ;
hence p . x = q . x by A12; :: thesis: verum
end;
suppose ( p . x = 0 & q . x = 0 ) ; :: thesis: p . b1 = q . b1
hence p . x = q . x ; :: thesis: verum
end;
end;
end;
hence contradiction by A4, A5, A6, FUNCT_1:2; :: thesis: verum
end;
consider j being Nat such that
A13: S1[j] and
A14: for k being Nat st S1[k] holds
k <= j from A15: (SgmX ((),(() \/ ()))) . j in rng (SgmX ((),(() \/ ()))) by ;
then reconsider J = (SgmX ((),(() \/ ()))) . 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 ) )
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 ; :: 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
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 :: thesis: ( not k in support p implies k in support q )end;
then k in () \/ () by XBOOLE_0:def 3;
then consider m being Nat such that
A22: m in dom (SgmX ((),(() \/ ()))) and
A23: (SgmX ((),(() \/ ()))) . m = k by ;
A24: m <= j by A14, A19, A22, A23;
m <> j by ;
then m < j by ;
then [((SgmX ((),(() \/ ()))) /. m),((SgmX ((),(() \/ ()))) /. j)] in RelIncl n by ;
then [((SgmX ((),(() \/ ()))) . m),((SgmX ((),(() \/ ()))) /. j)] in RelIncl n by ;
then [((SgmX ((),(() \/ ()))) . m),((SgmX ((),(() \/ ()))) . j)] in RelIncl n by ;
then (SgmX ((),(() \/ ()))) . m c= (SgmX ((),(() \/ ()))) . j by ;
hence contradiction by A17, A23, ORDINAL1:5; :: thesis: verum
end;
then q . J <= p . J by A3, A9, A15, Def6;
hence q . J < p . J by ; :: 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 Def6; :: 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 ; :: according to BAGORDER:def 5 :: thesis: ( ( for a being bag of n holds [(),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 :: thesis: for a being bag of n holds [(),a] in InvLexOrder n
let a be bag of n; :: thesis: [(),b1] in InvLexOrder n
per cases ( EmptyBag n = a or EmptyBag n <> a ) ;
suppose A25: EmptyBag n <> a ; :: thesis: [(),b1] in InvLexOrder n
set s = SgmX ((),());
A26: field () = n by WELLORD2:def 1;
RelIncl n is being_linear-order by ORDERS_1:19;
then A27: RelIncl n linearly_orders support a by ;
then A28: rng (SgmX ((),())) = support a by PRE_POLY:def 2;
then rng (SgmX ((),())) <> {} by ;
then A29: len (SgmX ((),())) in dom (SgmX ((),())) by ;
then A30: (SgmX ((),())) . (len (SgmX ((),()))) in rng (SgmX ((),())) by FUNCT_1:3;
then reconsider j = (SgmX ((),())) . (len (SgmX ((),()))) as Ordinal by A28;
now :: thesis: ex j being Ordinal st
( j in n & () . j < a . j & ( for k being Ordinal st j in k & k in n holds
() . k = a . k ) )
take j = j; :: thesis: ( j in n & () . j < a . j & ( for k being Ordinal st j in k & k in n holds
() . k = a . k ) )

thus j in n by ; :: thesis: ( () . j < a . j & ( for k being Ordinal st j in k & k in n holds
() . k = a . k ) )

A31: a . j <> 0 by ;
(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
() . k = a . k

let k be Ordinal; :: thesis: ( j in k & k in n implies () . k = a . k )
assume that
A32: j in k and
A33: k in n ; :: thesis: () . k = a . k
A34: j c= k by ;
now :: thesis: not () . k <> a . k
assume (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 ((),())) and
A36: (SgmX ((),())) . i = k by ;
A37: i <= len (SgmX ((),())) by ;
per cases ( i = len (SgmX ((),())) or i < len (SgmX ((),())) ) by ;
suppose i = len (SgmX ((),())) ; :: thesis: contradiction
end;
suppose i < len (SgmX ((),())) ; :: thesis: contradiction
then [((SgmX ((),())) /. i),((SgmX ((),())) /. (len (SgmX ((),()))))] in RelIncl n by ;
then [((SgmX ((),())) . i),((SgmX ((),())) /. (len (SgmX ((),()))))] in RelIncl n by ;
then [((SgmX ((),())) . i),((SgmX ((),())) . (len (SgmX ((),()))))] in RelIncl n by ;
then k c= j by ;
then j = k by ;
hence contradiction by A32; :: thesis: verum
end;
end;
end;
hence (EmptyBag n) . k = a . k ; :: thesis: verum
end;
hence [(),a] in InvLexOrder n by Def6; :: thesis: verum
end;
end;
end;
hence for a being bag of n holds [(),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 :: thesis: 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 [(b1 + b3),(b2 + b3)] in InvLexOrder n )
assume A38: [a,b] in InvLexOrder n ; :: thesis: [(b1 + b3),(b2 + b3)] in InvLexOrder n
per cases ( a = b or a <> b ) ;
suppose A39: a = b ; :: thesis: [(b1 + b3),(b2 + b3)] in InvLexOrder n
a + c in Bags n by PRE_POLY:def 12;
hence [(a + c),(b + c)] in InvLexOrder n by ; :: thesis: verum
end;
suppose a <> b ; :: thesis: [(b1 + b3),(b2 + b3)] 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 ;
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 ) )
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 ; :: 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 Def6; :: 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