let IT1, IT2 be TermOrder of n; :: thesis: ( ( for a, b being bag of n holds

( [a,b] in IT1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) & ( for a, b being bag of n holds

( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) implies IT1 = IT2 )

assume that

A36: for a, b being bag of n holds

( [a,b] in IT1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) and

A37: for a, b being bag of n holds

( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ; :: thesis: IT1 = IT2

( [a,b] in IT1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) & ( for a, b being bag of n holds

( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) implies IT1 = IT2 )

assume that

A36: for a, b being bag of n holds

( [a,b] in IT1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) and

A37: for a, b being bag of n holds

( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ; :: thesis: IT1 = IT2

now :: thesis: for a, b being object holds

( ( [a,b] in IT1 implies [a,b] in IT2 ) & ( [a,b] in IT2 implies [a,b] in IT1 ) )

hence
IT1 = IT2
by RELAT_1:def 2; :: thesis: verum( ( [a,b] in IT1 implies [a,b] in IT2 ) & ( [a,b] in IT2 implies [a,b] in IT1 ) )

let a, b be object ; :: thesis: ( ( [a,b] in IT1 implies [a,b] in IT2 ) & ( [a,b] in IT2 implies [a,b] in IT1 ) )

then A41: a in dom IT2 by XTUPLE_0:def 12;

b in rng IT2 by A40, XTUPLE_0:def 13;

then reconsider a9 = a, b9 = b as bag of n by A41;

( TotDegree a9 < TotDegree b9 or ( TotDegree a9 = TotDegree b9 & [a9,b9] in o ) ) by A37, A40;

hence [a,b] in IT1 by A36; :: thesis: verum

end;hereby :: thesis: ( [a,b] in IT2 implies [a,b] in IT1 )

assume A40:
[a,b] in IT2
; :: thesis: [a,b] in IT1assume A38:
[a,b] in IT1
; :: thesis: [a,b] in IT2

then A39: a in dom IT1 by XTUPLE_0:def 12;

b in rng IT1 by A38, XTUPLE_0:def 13;

then reconsider a9 = a, b9 = b as bag of n by A39;

( TotDegree a9 < TotDegree b9 or ( TotDegree a9 = TotDegree b9 & [a9,b9] in o ) ) by A36, A38;

hence [a,b] in IT2 by A37; :: thesis: verum

end;then A39: a in dom IT1 by XTUPLE_0:def 12;

b in rng IT1 by A38, XTUPLE_0:def 13;

then reconsider a9 = a, b9 = b as bag of n by A39;

( TotDegree a9 < TotDegree b9 or ( TotDegree a9 = TotDegree b9 & [a9,b9] in o ) ) by A36, A38;

hence [a,b] in IT2 by A37; :: thesis: verum

then A41: a in dom IT2 by XTUPLE_0:def 12;

b in rng IT2 by A40, XTUPLE_0:def 13;

then reconsider a9 = a, b9 = b as bag of n by A41;

( TotDegree a9 < TotDegree b9 or ( TotDegree a9 = TotDegree b9 & [a9,b9] in o ) ) by A37, A40;

hence [a,b] in IT1 by A36; :: thesis: verum