defpred S₁[ object , object ] means ( $1 = $2 or ex p, q being Element of Bags n st
( $1 = p & $2 = q & ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) );
consider ILO being Relation of (Bags n),(Bags n) such that
A1: for x, y being object holds
( [x,y] in ILO iff ( x in Bags n & y in Bags n & S₁[x,y] ) ) from RELSET_1:sch 1();
A2: ILO is_reflexive_in Bags n by A1;
A3: ILO is_antisymmetric_in Bags n

proof

let x, y be object ; :: according to RELAT_2:def 4 :: thesis:
assume that
x in Bags n and
y in Bags n and
A4: [x,y] in ILO and
A5: [y,x] in ILO ; :: thesis:

per cases ;

suppose x = y ; :: thesis:

hence x = y ; :: thesis:

end;

suppose A6: not x = y ; :: thesis:

then consider p, q being Element of Bags n such that
A7: x = p and
A8: y = q and
A9: ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) by A1, A4;
ex q9, p9 being Element of Bags n st
( y = q9 & x = p9 & ex i being Ordinal st
( i in n & q9 . i < p9 . i & ( for k being Ordinal st i in k & k in n holds
q9 . k = p9 . k ) ) ) by A1, A5, A6;
then consider i being Ordinal such that
A10: i in n and
A11: q . i < p . i and
A12: for k being Ordinal st i in k & k in n holds
q . k = p . k by A7, A8;
consider j being Ordinal such that
A13: j in n and
A14: p . j < q . j and
A15: for k being Ordinal st j in k & k in n holds
p . k = q . k by A9;

now :: thesis:

per cases by ORDINAL1:14;

suppose i in j ; :: thesis:

hence i = j by A12, A13, A14; :: thesis:

end;

suppose i = j ; :: thesis:

hence i = j ; :: thesis:

end;

suppose j in i ; :: thesis:

hence i = j by A10, A11, A15; :: thesis:

end;

hence x = y by A11, A14; :: thesis:

end;

A16: ILO is_transitive_in Bags n

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis:
assume that
x in Bags n and
y in Bags n and
z in Bags n and
A17: [x,y] in ILO and
A18: [y,z] in ILO ; :: thesis:

per cases ;

suppose x = y ; :: thesis:

hence [x,z] in ILO by A18; :: thesis:

end;

suppose x <> y ; :: thesis:

then consider p, q being Element of Bags n such that
A19: x = p and
A20: y = q and
A21: ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) by A1, A17;
consider i being Ordinal such that
A22: i in n and
A23: p . i < q . i and
A24: for k being Ordinal st i in k & k in n holds
p . k = q . k by A21;

now :: thesis:

per cases ;

suppose y = z ; :: thesis:

hence [x,z] in ILO by A17; :: thesis:

end;

suppose y <> z ; :: thesis:

then consider q9, r being Element of Bags n such that
A25: y = q9 and
A26: z = r and
A27: ex i being Ordinal st
( i in n & q9 . i < r . i & ( for k being Ordinal st i in k & k in n holds
q9 . k = r . k ) ) by A1, A18;
consider j being Ordinal such that
A28: j in n and
A29: q9 . j < r . j and
A30: for k being Ordinal st j in k & k in n holds
q9 . k = r . k by A27;

now :: thesis:

per cases by ORDINAL1:14;

suppose A31: i in j ; :: thesis:

then A32: p . j < r . j by A20, A24, A25, A28, A29;

now :: thesis:

let k be Ordinal; :: thesis:
assume that
A33: j in k and
A34: k in n ; :: thesis:
A35: q . k = r . k by A20, A25, A30, A33, A34;
i in k by A31, A33, ORDINAL1:10;
hence p . k = r . k by A24, A34, A35; :: thesis:

end;

hence [x,z] in ILO by A1, A19, A26, A28, A32; :: thesis:

end;

suppose A36: i = j ; :: thesis:

now :: thesis:

take p = p; :: thesis:
take r = r; :: thesis:
thus ( x = p & z = r ) by A19, A26; :: thesis:
take j = j; :: thesis:
thus j in n by A28; :: thesis:
thus p . j < r . j by A20, A23, A25, A29, A36, XXREAL_0:2; :: thesis:

now :: thesis:

let k be Ordinal; :: thesis:
assume that
A37: j in k and
A38: k in n ; :: thesis:
p . k = q . k by A24, A36, A37, A38;
hence p . k = r . k by A20, A25, A30, A37, A38; :: thesis:

end;

hence for k being Ordinal st j in k & k in n holds
p . k = r . k ; :: thesis:

end;

hence [x,z] in ILO by A1; :: thesis:

end;

suppose A39: j in i ; :: thesis:

then A40: p . i < r . i by A20, A22, A23, A25, A30;

now :: thesis:

let k be Ordinal; :: thesis:
assume that
A41: i in k and
A42: k in n ; :: thesis:
A43: p . k = q . k by A24, A41, A42;
j in k by A39, A41, ORDINAL1:10;
hence p . k = r . k by A20, A25, A30, A42, A43; :: thesis:

end;

hence [x,z] in ILO by A1, A19, A22, A26, A40; :: thesis:

end;

hence [x,z] in ILO ; :: thesis:

end;

hence [x,z] in ILO ; :: thesis:

end;

A44: dom ILO = Bags n by A2, ORDERS_1:13;
field ILO = Bags n by A2, ORDERS_1:13;
then reconsider ILO = ILO as TermOrder of n by A2, A3, A16, A44, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take ILO ; :: thesis:
let x, y be bag of n; :: thesis:

hereby :: thesis:

assume A45: [x,y] in ILO ; :: thesis:

now :: thesis:

assume x <> y ; :: thesis:
then ex p, q being Element of Bags n st
( x = p & y = q & ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) by A1, A45;
hence ex i being Ordinal st
( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds
x . k = y . k ) ) ; :: thesis:

end;

hence ( x = y or ex i being Ordinal st
( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds
x . k = y . k ) ) ) ; :: thesis:

end;

assume A46: ( x = y or ex i being Ordinal st
( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds
x . k = y . k ) ) ) ; :: thesis:

A47: now :: thesis:

assume A48: x <> y ; :: thesis:
thus ex p, q being Element of Bags n st
( x = p & y = q & ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) :: thesis:

proof

reconsider x9 = x, y9 = y as Element of Bags n by PRE_POLY:def 12;
take x9 ; :: thesis:
take y9 ; :: thesis:
thus ( x = x9 & y = y9 ) ; :: thesis:
thus ex i being Ordinal st
( i in n & x9 . i < y9 . i & ( for k being Ordinal st i in k & k in n holds
x9 . k = y9 . k ) ) by A46, A48; :: thesis:

end;

x in Bags n by PRE_POLY:def 12;
hence [x,y] in ILO by A1, A47; :: thesis: