defpred S_{1}[ 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_{1}[x,y] ) )
from RELSET_1:sch 1();

A2: ILO is_reflexive_in Bags n by A1;

A3: ILO is_antisymmetric_in Bags n

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: for p, q being bag of n holds

( [p,q] in ILO iff ( p = q or 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 ) ) ) )

let x, y be bag of n; :: thesis: ( [x,y] in ILO iff ( 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 ) ) ) )

( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) ) ) ; :: thesis: [x,y] in ILO

hence [x,y] in ILO by A1, A47; :: thesis: verum

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

A2: ILO is_reflexive_in Bags n by A1;

A3: ILO is_antisymmetric_in Bags n

proof

A16:
ILO is_transitive_in Bags n
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in Bags n or not y in Bags n or not [x,y] in ILO or not [y,x] in ILO or x = y )

assume that

x in Bags n and

y in Bags n and

A4: [x,y] in ILO and

A5: [y,x] in ILO ; :: thesis: x = y

end;assume that

x in Bags n and

y in Bags n and

A4: [x,y] in ILO and

A5: [y,x] in ILO ; :: thesis: x = y

per cases
( x = y or not x = y )
;

end;

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

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;

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

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

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

proof

A44:
dom ILO = Bags n
by A2, ORDERS_1:13;
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in Bags n or not y in Bags n or not z in Bags n or not [x,y] in ILO or not [y,z] in ILO or [x,z] in ILO )

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: [x,z] in ILO

end;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: [x,z] in ILO

per cases
( x = y or x <> y )
;

end;

suppose
x <> y
; :: thesis: [x,z] in ILO

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;

end;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: [x,z] in ILOend;

hence
[x,z] in ILO
; :: thesis: verumper cases
( y = z or y <> z )
;

end;

suppose
y <> z
; :: thesis: [x,z] in ILO

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;

end;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: [x,z] in ILOend;

hence
[x,z] in ILO
; :: thesis: verumper cases
( i in j or i = j or j in i )
by ORDINAL1:14;

end;

suppose A31:
i in j
; :: thesis: [x,z] in ILO

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

end;now :: thesis: for k being Ordinal st j in k & k in n holds

p . k = r . k

hence
[x,z] in ILO
by A1, A19, A26, A28, A32; :: thesis: verump . k = r . k

let k be Ordinal; :: thesis: ( j in k & k in n implies p . k = r . k )

assume that

A33: j in k and

A34: k in n ; :: thesis: p . k = r . k

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: verum

end;assume that

A33: j in k and

A34: k in n ; :: thesis: p . k = r . k

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: verum

suppose A36:
i = j
; :: thesis: [x,z] in ILO

end;

now :: thesis: ex p, r being Element of Bags n st

( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

hence
[x,z] in ILO
by A1; :: thesis: verum( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

take p = p; :: thesis: ex r being Element of Bags n st

( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

take r = r; :: thesis: ( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

thus ( x = p & z = r ) by A19, A26; :: thesis: ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) )

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

p . k = r . k ) )

thus j in n by A28; :: thesis: ( p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) )

thus p . j < r . j by A20, A23, A25, A29, A36, XXREAL_0:2; :: thesis: for k being Ordinal st j in k & k in n holds

p . k = r . k

p . k = r . k ; :: thesis: verum

end;( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

take r = r; :: thesis: ( x = p & z = r & ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) ) )

thus ( x = p & z = r ) by A19, A26; :: thesis: ex j being Ordinal st

( j in n & p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) )

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

p . k = r . k ) )

thus j in n by A28; :: thesis: ( p . j < r . j & ( for k being Ordinal st j in k & k in n holds

p . k = r . k ) )

thus p . j < r . j by A20, A23, A25, A29, A36, XXREAL_0:2; :: thesis: for k being Ordinal st j in k & k in n holds

p . k = r . k

now :: thesis: for k being Ordinal st j in k & k in n holds

p . k = r . k

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

let k be Ordinal; :: thesis: ( j in k & k in n implies p . k = r . k )

assume that

A37: j in k and

A38: k in n ; :: thesis: p . k = r . k

p . k = q . k by A24, A36, A37, A38;

hence p . k = r . k by A20, A25, A30, A37, A38; :: thesis: verum

end;assume that

A37: j in k and

A38: k in n ; :: thesis: p . k = r . k

p . k = q . k by A24, A36, A37, A38;

hence p . k = r . k by A20, A25, A30, A37, A38; :: thesis: verum

p . k = r . k ; :: thesis: verum

suppose A39:
j in i
; :: thesis: [x,z] in ILO

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

end;now :: thesis: for k being Ordinal st i in k & k in n holds

p . k = r . k

hence
[x,z] in ILO
by A1, A19, A22, A26, A40; :: thesis: verump . k = r . k

let k be Ordinal; :: thesis: ( i in k & k in n implies p . k = r . k )

assume that

A41: i in k and

A42: k in n ; :: thesis: p . k = r . k

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: verum

end;assume that

A41: i in k and

A42: k in n ; :: thesis: p . k = r . k

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: verum

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: for p, q being bag of n holds

( [p,q] in ILO iff ( p = q or 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 ) ) ) )

let x, y be bag of n; :: thesis: ( [x,y] in ILO iff ( 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 ) ) ) )

hereby :: thesis: ( ( 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 ) ) ) implies [x,y] in ILO )

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 ) ) ) implies [x,y] in ILO )

assume A45:
[x,y] in ILO
; :: thesis: ( 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 ) ) )

( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) ) ) ; :: thesis: verum

end;( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) ) )

now :: thesis: ( x <> y implies 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 ) ) )

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

assume
x <> y
; :: thesis: 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 ) )

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: verum

end;( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) )

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: verum

( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) ) ) ; :: thesis: verum

( i in n & x . i < y . i & ( for k being Ordinal st i in k & k in n holds

x . k = y . k ) ) ) ; :: thesis: [x,y] in ILO

A47: now :: thesis: ( x <> y implies 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 ) ) ) )

x in Bags n
by PRE_POLY:def 12;( 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 ) ) ) )

assume A48:
x <> y
; :: thesis: 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 ) ) )

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: verum

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

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: verum

proof

reconsider x9 = x, y9 = y as Element of Bags n by PRE_POLY:def 12;

take x9 ; :: thesis: ex q being Element of Bags n st

( x = x9 & y = q & ex i being Ordinal st

( i in n & x9 . i < q . i & ( for k being Ordinal st i in k & k in n holds

x9 . k = q . k ) ) )

take y9 ; :: thesis: ( x = x9 & y = y9 & 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 ) ) )

thus ( x = x9 & y = y9 ) ; :: thesis: 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 ) )

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: verum

end;take x9 ; :: thesis: ex q being Element of Bags n st

( x = x9 & y = q & ex i being Ordinal st

( i in n & x9 . i < q . i & ( for k being Ordinal st i in k & k in n holds

x9 . k = q . k ) ) )

take y9 ; :: thesis: ( x = x9 & y = y9 & 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 ) ) )

thus ( x = x9 & y = y9 ) ; :: thesis: 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 ) )

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: verum

hence [x,y] in ILO by A1, A47; :: thesis: verum