defpred S₁[ set , set ] means ex x', y' being bag of st
( x' = $1 & y' = $2 & ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) );
consider R being Relation of (Bags n) such that
A2: 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();

A3: now

now

let x be set ; :: thesis: ( x in Bags n implies [x,x] in R )
assume A4: x in Bags n ; :: thesis: [x,x] in R
reconsider x' = x as bag of by A4, POLYNOM1:def 14;

now

take x' = x'; :: thesis: ( x' = x & TotDegree x' = TotDegree x' & [x',x'] in o )
thus x' = x ; :: thesis: ( TotDegree x' = TotDegree x' & [x',x'] in o )
thus TotDegree x' = TotDegree x' ; :: thesis: [x',x'] in o
[(EmptyBag n),(EmptyBag n)] in o by ORDERS_1:12;
then [((EmptyBag n) + x'),((EmptyBag n) + x')] in o by A1;
then [x',((EmptyBag n) + x')] in o by POLYNOM1:57;
hence [x',x'] in o by POLYNOM1:57; :: thesis: verum

end;

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

end;

hence R is_reflexive_in Bags n by RELAT_2:def 1; :: thesis: ( R is_antisymmetric_in Bags n & R is_transitive_in Bags n )

now

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 A5: ( x in Bags n & y in Bags n & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
consider x', y' being bag of such that
A6: ( x' = x & y' = y ) and
A7: ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A2, A5;
consider y'', x'' being bag of such that
A8: ( y'' = y & x'' = x ) and
A9: ( TotDegree y'' < TotDegree x'' or ( TotDegree y'' = TotDegree x'' & [y'',x''] in o ) ) by A2, A5;

now

per cases ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A7;

suppose A10: TotDegree x' < TotDegree y' ; :: thesis: ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o )

now

per cases ( TotDegree y' < TotDegree x' or ( TotDegree y' = TotDegree x' & [y',x'] in o ) ) by A6, A8, A9;

suppose TotDegree y' < TotDegree x' ; :: thesis: contradiction

hence contradiction by A10; :: thesis: verum

end;

suppose ( TotDegree y' = TotDegree x' & [y',x'] in o ) ; :: thesis: contradiction

hence contradiction by A10; :: thesis: verum

end;

end;

end;

hence ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o ) ; :: thesis: verum

end;

suppose A11: ( TotDegree x' = TotDegree y' & [x',y'] in o ) ; :: thesis: ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o )

now

per cases ( TotDegree y' < TotDegree x' or ( TotDegree y' = TotDegree x' & [y',x'] in o ) ) by A6, A8, A9;

suppose TotDegree y' < TotDegree x' ; :: thesis: ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o )

hence ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o ) by A11; :: thesis: verum

end;

suppose ( TotDegree y' = TotDegree x' & [y',x'] in o ) ; :: thesis: ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o )

hence ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o ) by A11; :: thesis: verum

end;

end;

end;

hence ( TotDegree x' = TotDegree y' & [x',y'] in o & TotDegree y' = TotDegree x' & [y',x'] in o ) ; :: thesis: verum

end;

end;

end;

hence x = y by A5, A6, ORDERS_1:13; :: thesis: verum

end;

hence R is_antisymmetric_in Bags n by RELAT_2:def 4; :: thesis: R is_transitive_in Bags n

now

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 A12: ( x in Bags n & y in Bags n & z in Bags n & [x,y] in R & [y,z] in R ) ; :: thesis: [b₁,b₃] in R
consider x', y' being bag of such that
A13: ( x' = x & y' = y & ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) ) by A2, A12;
consider y'', z' being bag of such that
A14: ( y'' = y & z' = z & ( TotDegree y'' < TotDegree z' or ( TotDegree y'' = TotDegree z' & [y'',z'] in o ) ) ) by A2, A12;

per cases ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A13;

suppose A15: TotDegree x' < TotDegree y' ; :: thesis: [b₁,b₃] in R

now

per cases ( TotDegree y' < TotDegree z' or ( TotDegree y' = TotDegree z' & [y',z'] in o ) ) by A13, A14;

suppose TotDegree y' < TotDegree z' ; :: thesis: [x,z] in R

then TotDegree x' < TotDegree z' by A15, XXREAL_0:2;
hence [x,z] in R by A2, A12, A13, A14; :: thesis: verum

end;

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

hence [x,z] in R by A2, A12, A13, A14, A15; :: thesis: verum

end;

end;

end;

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

end;

suppose A16: ( TotDegree x' = TotDegree y' & [x',y'] in o ) ; :: thesis: [b₁,b₃] in R

now

per cases ( TotDegree y' < TotDegree z' or ( TotDegree y' = TotDegree z' & [y',z'] in o ) ) by A13, A14;

suppose TotDegree y' < TotDegree z' ; :: thesis: [x,z] in R

hence [x,z] in R by A2, A12, A13, A14, A16; :: thesis: verum

end;

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

then [x',z'] in o by A12, A13, A14, A16, ORDERS_1:14;
hence [x,z] in R by A2, A12, A13, A14, A16; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence R is_transitive_in Bags n by RELAT_2:def 8; :: thesis: verum

end;

then ( dom R = Bags n & field R = Bags n ) by ORDERS_1:98;
then reconsider R = R as TermOrder of n by A3, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take R ; :: thesis: for a, b being bag of 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 ; :: 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 consider x', y' being bag of such that
A17: ( x' = a & y' = b ) and
A18: ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A2;
thus ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) by A17, A18; :: thesis: verum

end;

assume A19: ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ; :: thesis: [a,b] in R
( a in Bags n & b in Bags n ) by POLYNOM1:def 14;
hence [a,b] in R by A2, A19; :: thesis: verum