let IT1, IT2 be TermOrder of n; :: thesis: ( ( for a, b being bag of 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 holds
( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) implies IT1 = IT2 )
assume that
A20: for a, b being bag of holds
( [a,b] in IT1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) and
A21: for a, b being bag of holds
( [a,b] in IT2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ; :: thesis: IT1 = IT2

now

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

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

assume A22: [a,b] in IT1 ; :: thesis: [a,b] in IT2
then ( a in dom IT1 & b in rng IT1 ) by RELAT_1:def 4, RELAT_1:def 5;
then reconsider a' = a, b' = b as bag of by POLYNOM1:def 14;
( TotDegree a' < TotDegree b' or ( TotDegree a' = TotDegree b' & [a',b'] in o ) ) by A20, A22;
hence [a,b] in IT2 by A21; :: thesis: verum

end;

assume A23: [a,b] in IT2 ; :: thesis: [a,b] in IT1
then ( a in dom IT2 & b in rng IT2 ) by RELAT_1:def 4, RELAT_1:def 5;
then reconsider a' = a, b' = b as bag of by POLYNOM1:def 14;
( TotDegree a' < TotDegree b' or ( TotDegree a' = TotDegree b' & [a',b'] in o ) ) by A21, A23;
hence [a,b] in IT1 by A20; :: thesis: verum

end;

hence IT1 = IT2 by RELAT_1:def 2; :: thesis: verum