defpred S₁[ set , set ] 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
A1: for x, y being set holds
( [x,y] in R iff ( x in Bags n & y in Bags n & S₁[x,y] ) ) from RELSET_1:sch 1();

A2: now :: thesis: for x being set st x in Bags n holds
[x,x] in R

let x be set ; :: thesis: ( x in Bags n implies [x,x] in R )
assume A3: x in Bags n ; :: thesis: [x,x] in R
reconsider x9 = x as bag of n by A3;

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 B1;
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 A1, A3; :: thesis: verum

end;

A4: now :: thesis: for x, y being set st x in Bags n & y in Bags n & [x,y] in R & [y,x] in R holds
x = y

let x, y be set ; :: thesis: ( x in Bags n & y in Bags n & [x,y] in R & [y,x] in R implies x = y )
assume that
A5: x in Bags n and
A6: y in Bags n and
A7: [x,y] in R and
A8: [y,x] in R ; :: thesis: x = y
consider x9, y9 being bag of n such that
A9: x9 = x and
A10: y9 = y and
A11: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A1, A7;
A12: 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 A1, A8;

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

suppose A13: 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 A9, A10, A12;

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

hence contradiction by A13; :: thesis: verum

end;

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

hence contradiction by A13; :: 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 A14: ( 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 A9, A10, A12;

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 A14; :: 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 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;

end;

end;

hence x = y by A5, A6, A9, A10, ORDERS_1:4; :: thesis: verum

end;

A15: now :: thesis: for x, y, z being set 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 set ; :: 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
A16: x in Bags n and
A17: y in Bags n and
A18: z in Bags n and
A19: [x,y] in R and
A20: [y,z] in R ; :: thesis: [b₁,b₃] in R
consider x9, y9 being bag of n such that
A21: x9 = x and
A22: y9 = y and
A23: ( TotDegree x9 < TotDegree y9 or ( TotDegree x9 = TotDegree y9 & [x9,y9] in o ) ) by A1, A19;
consider y99, z9 being bag of n such that
A24: y99 = y and
A25: z9 = z and
A26: ( TotDegree y99 < TotDegree z9 or ( TotDegree y99 = TotDegree z9 & [y99,z9] in o ) ) by A1, A20;

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

suppose A27: 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 A22, A24, A26;

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

then TotDegree x9 < TotDegree z9 by A27, XXREAL_0:2;
hence [x,z] in R by A1, A16, A18, A21, A25; :: thesis: verum

end;

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

hence [x,z] in R by A1, A16, A18, A21, A25, A27; :: thesis: verum

end;

end;

end;

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

end;

suppose A28: ( 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 A22, A24, A26;

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

hence [x,z] in R by A1, A16, A18, A21, A25, A28; :: thesis: verum

end;

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

then [x9,z9] in o by A16, A17, A18, A21, A22, A25, A28, ORDERS_1:5;
hence [x,z] in R by A1, A16, A18, A21, A22, A24, A25, A26, A28; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

A29: R is_reflexive_in Bags n by A2, RELAT_2:def 1;
A30: R is_antisymmetric_in Bags n by A4, RELAT_2:def 4;
A31: R is_transitive_in Bags n by A15, RELAT_2:def 8;
A32: dom R = Bags n by A29, ORDERS_1:13;
field R = Bags n by A29, ORDERS_1:13;
then reconsider R = R as TermOrder of n by A29, A30, A31, A32, 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 A1;
hence ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: verum

end;

assume A33: ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: [a,b] in R
A34: a in Bags n by PRE_POLY:def 12;
b in Bags n by PRE_POLY:def 12;
hence [a,b] in R by A1, A33, A34; :: thesis: verum