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

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 n by A4, PRE_POLY:def 12;

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 PRE_POLY:53;
hence [x',x'] in o by PRE_POLY:53; :: thesis: verum

end;

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

end;

A5: 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 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 x', y' being bag of n such that
A10: x' = x and
A11: y' = y and
A12: ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A2, A8;
A13: ex y'', x'' being bag of n st
( y'' = y & x'' = x & ( TotDegree y'' < TotDegree x'' or ( TotDegree y'' = TotDegree x'' & [y'',x''] in o ) ) ) by A2, A9;

now

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

suppose A14: 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 A10, A11, A13;

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

hence contradiction by A14; :: thesis: verum

end;

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

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

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 A15; :: 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 A15; :: 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 A6, A7, A10, A11, ORDERS_1:13; :: thesis: verum

end;

A16: 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 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 x', y' being bag of n such that
A22: x' = x and
A23: y' = y and
A24: ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] in o ) ) by A2, A20;
consider y'', z' being bag of n such that
A25: y'' = y and
A26: z' = z and
A27: ( TotDegree y'' < TotDegree z' or ( TotDegree y'' = TotDegree z' & [y'',z'] in o ) ) by A2, A21;

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

suppose A28: 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 A23, A25, A27;

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

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

end;

suppose ( TotDegree y' = TotDegree z' & [y',z'] 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 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 A23, A25, A27;

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

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

end;

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

then [x',z'] in o by A17, A18, A19, A22, A23, A26, A29, ORDERS_1:14;
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, RELAT_2:def 1;
A31: R is_antisymmetric_in Bags n by A5, RELAT_2:def 4;
A32: R is_transitive_in Bags n by A16, RELAT_2:def 8;
A33: dom R = Bags n by A30, ORDERS_1:98;
field R = Bags n by A30, ORDERS_1:98;
then reconsider R = R as TermOrder of n by A30, A31, A32, A33, PARTFUN1:def 4, 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 x', y' being bag of n st
( x' = a & y' = b & ( TotDegree x' < TotDegree y' or ( TotDegree x' = TotDegree y' & [x',y'] 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