defpred S₁[ 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₁[x,y] ) ) from RELSET_1:sch 1();

A3: now :: thesis: for x being object st x in Bags n holds
[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;

now :: thesis: ex x9 being bag of n st
( 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;

hence [x,x] in R by A2, A4; :: thesis: verum

end;

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

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;

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

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

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

now :: thesis: contradiction

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

suppose TotDegree y9 < TotDegree x9 ; :: thesis: contradiction

hence contradiction by A14; :: thesis: verum

end;

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

hence contradiction by A14; :: thesis: verum

end;

end;

end;

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

end;

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 )

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

hence x = y by A6, A7, A10, A11, ORDERS_1:4; :: thesis: verum

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

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₁,b₃] 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₁,b₃] 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;

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

suppose A28: TotDegree x9 < TotDegree y9 ; :: thesis: [b₁,b₃] in R

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

per cases ( TotDegree y9 < TotDegree z9 or ( TotDegree y9 = TotDegree z9 & [y9,z9] in o ) ) by A23, A25, A27;

suppose TotDegree y9 < TotDegree z9 ; :: thesis: [x,z] in R

then TotDegree x9 < TotDegree z9 by A28, XXREAL_0:2;
hence [x,z] in R by A2, A17, A19, A22, A26; :: thesis: verum

end;

suppose ( TotDegree y9 = TotDegree z9 & [y9,z9] in o ) ; :: thesis: [x,z] in R

hence [x,z] in R by A2, A17, A19, A22, A26, A28; :: thesis: verum

end;

end;

end;

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

end;

suppose A29: ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ; :: thesis: [b₁,b₃] in R

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

per cases ( TotDegree y9 < TotDegree z9 or ( TotDegree y9 = TotDegree z9 & [y9,z9] in o ) ) by A23, A25, A27;

suppose TotDegree y9 < TotDegree z9 ; :: thesis: [x,z] in R

hence [x,z] in R by A2, A17, A19, A22, A26, A29; :: thesis: verum

end;

suppose ( TotDegree y9 = TotDegree z9 & [y9,z9] in o ) ; :: thesis: [x,z] in R

then [x9,z9] in o by A17, A18, A19, A22, A23, A26, A29, ORDERS_1:5;
hence [x,z] in R by A2, A17, A19, A22, A23, A25, A26, A27, A29; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

A30: R is_reflexive_in Bags n by A3;
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 [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;

assume A34: ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: [a,b] in R
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