defpred S_{1}[ object , object ] means ex x9, y9 being bag of n st

( x9 = $1 & y9 = $2 & ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) );

consider R being Relation of (Bags n) such that

A2: for x, y being object holds

( [x,y] in R iff ( x in Bags n & y in Bags n & S_{1}[x,y] ) )
from RELSET_1:sch 1();

A31: R is_antisymmetric_in Bags n by A5;

A32: R is_transitive_in Bags n by A16;

A33: dom R = Bags n by A30, ORDERS_1:13;

field R = Bags n by A30, ORDERS_1:13;

then reconsider R = R as TermOrder of n by A30, A31, A32, A33, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

take R ; :: thesis: for a, b being bag of n holds

( [a,b] in R iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

let a, b be bag of n; :: thesis: ( [a,b] in R iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

A35: a in Bags n by PRE_POLY:def 12;

b in Bags n by PRE_POLY:def 12;

hence [a,b] in R by A2, A34, A35; :: thesis: verum

( x9 = $1 & y9 = $2 & ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) );

consider R being Relation of (Bags n) such that

A2: for x, y being object holds

( [x,y] in R iff ( x in Bags n & y in Bags n & S

A3: now :: thesis: for x being object st x in Bags n holds

[x,x] in R

[x,x] in R

let x be object ; :: thesis: ( x in Bags n implies [x,x] in R )

assume A4: x in Bags n ; :: thesis: [x,x] in R

reconsider x9 = x as bag of n by A4;

end;assume A4: x in Bags n ; :: thesis: [x,x] in R

reconsider x9 = x as bag of n by A4;

now :: thesis: ex x9 being bag of n st

( x9 = x & TotDegree x9 = TotDegree x9 & [x9,x9] in o )

hence
[x,x] in R
by A2, A4; :: thesis: verum( x9 = x & TotDegree x9 = TotDegree x9 & [x9,x9] in o )

take x9 = x9; :: thesis: ( x9 = x & TotDegree x9 = TotDegree x9 & [x9,x9] in o )

thus x9 = x ; :: thesis: ( TotDegree x9 = TotDegree x9 & [x9,x9] in o )

thus TotDegree x9 = TotDegree x9 ; :: thesis: [x9,x9] in o

[(EmptyBag n),(EmptyBag n)] in o by ORDERS_1:3;

then [((EmptyBag n) + x9),((EmptyBag n) + x9)] in o by A1;

then [x9,((EmptyBag n) + x9)] in o by PRE_POLY:53;

hence [x9,x9] in o by PRE_POLY:53; :: thesis: verum

end;thus x9 = x ; :: thesis: ( TotDegree x9 = TotDegree x9 & [x9,x9] in o )

thus TotDegree x9 = TotDegree x9 ; :: thesis: [x9,x9] in o

[(EmptyBag n),(EmptyBag n)] in o by ORDERS_1:3;

then [((EmptyBag n) + x9),((EmptyBag n) + x9)] in o by A1;

then [x9,((EmptyBag n) + x9)] in o by PRE_POLY:53;

hence [x9,x9] in o by PRE_POLY:53; :: thesis: verum

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

x = y

x = y

let x, y be object ; :: thesis: ( x in Bags n & y in Bags n & [x,y] in R & [y,x] in R implies x = y )

assume that

A6: x in Bags n and

A7: y in Bags n and

A8: [x,y] in R and

A9: [y,x] in R ; :: thesis: x = y

consider x9, y9 being bag of n such that

A10: x9 = x and

A11: y9 = y and

A12: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A2, A8;

A13: ex y99, x99 being bag of n st

( y99 = y & x99 = x & ( TotDegree y99 < TotDegree x99 or ( TotDegree y99 = TotDegree x99 & [y99,x99] in o ) ) ) by A2, A9;

end;assume that

A6: x in Bags n and

A7: y in Bags n and

A8: [x,y] in R and

A9: [y,x] in R ; :: thesis: x = y

consider x9, y9 being bag of n such that

A10: x9 = x and

A11: y9 = y and

A12: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A2, A8;

A13: ex y99, x99 being bag of n st

( y99 = y & x99 = x & ( TotDegree y99 < TotDegree x99 or ( TotDegree y99 = TotDegree x99 & [y99,x99] in o ) ) ) by A2, A9;

now :: thesis: ( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )end;

hence
x = y
by A6, A7, A10, A11, ORDERS_1:4; :: thesis: verumper cases
( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) )
by A12;

end;

suppose A14:
TotDegree x9 < TotDegree y9
; :: thesis: ( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )

end;

now :: thesis: contradiction

hence
( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )
; :: thesis: verumend;

suppose A15:
( TotDegree x9 = TotDegree y9 & [x9,y9] in o )
; :: thesis: ( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )

end;

now :: thesis: ( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )end;

hence
( TotDegree x9 = TotDegree y9 & [x9,y9] in o & TotDegree y9 = TotDegree x9 & [y9,x9] in o )
; :: thesis: verumper cases
( TotDegree y9 < TotDegree x9 or ( TotDegree y9 = TotDegree x9 & [y9,x9] in o ) )
by A10, A11, A13;

end;

A16: now :: thesis: for x, y, z being object st x in Bags n & y in Bags n & z in Bags n & [x,y] in R & [y,z] in R holds

[x,z] in R

A30:
R is_reflexive_in Bags n
by A3;[x,z] in R

let x, y, z be object ; :: thesis: ( x in Bags n & y in Bags n & z in Bags n & [x,y] in R & [y,z] in R implies [b_{1},b_{3}] in R )

assume that

A17: x in Bags n and

A18: y in Bags n and

A19: z in Bags n and

A20: [x,y] in R and

A21: [y,z] in R ; :: thesis: [b_{1},b_{3}] in R

consider x9, y9 being bag of n such that

A22: x9 = x and

A23: y9 = y and

A24: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A2, A20;

consider y99, z9 being bag of n such that

A25: y99 = y and

A26: z9 = z and

A27: ( TotDegree y99 < TotDegree z9 or ( TotDegree y99 = TotDegree z9 & [y99,z9] in o ) ) by A2, A21;

end;assume that

A17: x in Bags n and

A18: y in Bags n and

A19: z in Bags n and

A20: [x,y] in R and

A21: [y,z] in R ; :: thesis: [b

consider x9, y9 being bag of n such that

A22: x9 = x and

A23: y9 = y and

A24: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A2, A20;

consider y99, z9 being bag of n such that

A25: y99 = y and

A26: z9 = z and

A27: ( TotDegree y99 < TotDegree z9 or ( TotDegree y99 = TotDegree z9 & [y99,z9] in o ) ) by A2, A21;

per cases
( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) )
by A24;

end;

suppose A28:
TotDegree x9 < TotDegree y9
; :: thesis: [b_{1},b_{3}] in R

end;

now :: thesis: [x,z] in R

hence
[x,z] in R
; :: thesis: verumend;

suppose A29:
( TotDegree x9 = TotDegree y9 & [x9,y9] in o )
; :: thesis: [b_{1},b_{3}] in R

end;

now :: thesis: [x,z] in R

hence
[x,z] in R
; :: thesis: verumend;

A31: R is_antisymmetric_in Bags n by A5;

A32: R is_transitive_in Bags n by A16;

A33: dom R = Bags n by A30, ORDERS_1:13;

field R = Bags n by A30, ORDERS_1:13;

then reconsider R = R as TermOrder of n by A30, A31, A32, A33, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

take R ; :: thesis: for a, b being bag of n holds

( [a,b] in R iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

let a, b be bag of n; :: thesis: ( [a,b] in R iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

hereby :: thesis: ( ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) implies [a,b] in R )

assume A34:
( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) )
; :: thesis: [a,b] in Rassume
[a,b] in R
; :: thesis: ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) )

then ex x9, y9 being bag of n st

( x9 = a & y9 = b & ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) ) by A2;

hence ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: verum

end;then ex x9, y9 being bag of n st

( x9 = a & y9 = b & ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) ) by A2;

hence ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: verum

A35: a in Bags n by PRE_POLY:def 12;

b in Bags n by PRE_POLY:def 12;

hence [a,b] in R by A2, A34, A35; :: thesis: verum