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

now :: thesis:

let x, y be object ; :: thesis:
assume that
A1: x in Bags n and
A2: y in Bags n ; :: thesis:
reconsider p = x, q = y as bag of n by A1, A2;

now :: thesis:

proof

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

now :: thesis:

let x be object ; :: thesis:
assume x in n ; :: thesis:

per cases ;

suppose p . x <> 0 ; :: thesis:

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:

end;

suppose q . x <> 0 ; :: thesis:

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:

end;

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

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

end;

hence contradiction by A4, A5, A6, FUNCT_1:2; :: thesis:

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:3;
then reconsider J = (SgmX ((RelIncl n),((support p) \/ (support q)))) . j as Ordinal by A9;

now :: thesis:

take J = J; :: thesis:
thus J in n by A9, A15; :: thesis:

A16: now :: thesis:

let k be Ordinal; :: thesis:
assume that
A17: J in k and
A18: k in n and
A19: q . k <> p . k ; :: thesis:

now :: thesis:

assume that
A20: not k in support p and
A21: not k in support q ; :: thesis:
p . k = 0 by A20, PRE_POLY:def 7;
hence contradiction by A19, A21, PRE_POLY:def 7; :: thesis:

end;

end;

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

end;

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

end;

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

end;

hence InvLexOrder n is_strongly_connected_in Bags n ; :: according to BAGORDER:def 5 :: thesis:

now :: thesis:

let a be bag of n; :: thesis:

per cases ;

suppose EmptyBag n = a ; :: thesis:

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

end;

suppose A25: EmptyBag n <> a ; :: thesis:

now :: thesis:

take j = j; :: thesis:
thus j in n by A28, A30; :: thesis:
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:
let k be Ordinal; :: thesis:
assume that
A32: j in k and
A33: k in n ; :: thesis:
A34: j c= k by A32, ORDINAL1:def 2;

now :: thesis:

assume (EmptyBag n) . k <> a . k ; :: thesis:
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 by A37, XXREAL_0:1;

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

hence contradiction by A32, A36; :: thesis:

end;

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

end;

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

end;

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

end;

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

now :: thesis:

let a, b, c be bag of n; :: thesis:
assume A38: [a,b] in InvLexOrder n ; :: thesis:

per cases ;

suppose A39: a = b ; :: thesis:

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

end;

suppose a <> b ; :: thesis:

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;

now :: thesis:

take i = i; :: thesis:
thus i in n by A40; :: thesis:
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:
let k be Ordinal; :: thesis:
assume that
A44: i in k and
A45: k in n ; :: thesis:
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:

end;

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

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: