defpred S1[ 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 & S1[x,y] ) )
from RELSET_1:sch 1();
A5:
now for x, y being object st x in Bags n & y in Bags n & [x,y] in R & [y,x] in R holds
x = ylet x,
y be
object ;
( 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
;
x = yconsider 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;
hence
x = y
by A6, A7, A10, A11, ORDERS_1:4;
verum end;
A16:
now 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 Rlet x,
y,
z be
object ;
( x in Bags n & y in Bags n & z in Bags n & [x,y] in R & [y,z] in R implies [b1,b3] 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
;
[b1,b3] in Rconsider 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 A29:
(
TotDegree x9 = TotDegree y9 &
[x9,y9] in o )
;
[b1,b3] in Rnow [x,z] in Rper cases
( TotDegree y9 < TotDegree z9 or ( TotDegree y9 = TotDegree z9 & [y9,z9] in o ) )
by A23, A25, A27;
suppose
(
TotDegree y9 = TotDegree z9 &
[y9,z9] in o )
;
[x,z] in Rthen
[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;
verum end; end; end; hence
[x,z] in R
;
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
; 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; ( [a,b] in R iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )
assume A34:
( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) )
; [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; verum