let IT1, IT2 be TermOrder of n; :: thesis: ( ( for p, q being bag of holds
( [p,q] in IT1 iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) ) ) & ( for p, q being bag of holds
( [p,q] in IT2 iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) ) ) implies IT1 = IT2 )
assume that
A34: for p, q being bag of holds
( [p,q] in IT1 iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) ) and
A35: for p, q being bag of holds
( [p,q] in IT2 iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) ) ; :: thesis: IT1 = IT2

now

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

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

assume A36: [a,b] in IT1 ; :: thesis: [a,b] in IT2
then consider p, q being set such that
A37: ( [a,b] = [p,q] & p in Bags n & q in Bags n ) by RELSET_1:6;
reconsider p = p, q = q as bag of by A37, POLYNOM1:def 14;

per cases ( p = q or p <> q ) ;

suppose p = q ; :: thesis: [a,b] in IT2

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

end;

suppose p <> q ; :: thesis: [a,b] in IT2

then ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) by A34, A36, A37;
hence [a,b] in IT2 by A35, A37; :: thesis: verum

end;

end;

end;

assume A38: [a,b] in IT2 ; :: thesis: [b₁,b₂] in IT1
then consider p, q being set such that
A39: ( [a,b] = [p,q] & p in Bags n & q in Bags n ) by RELSET_1:6;
reconsider p = p, q = q as bag of by A39, POLYNOM1:def 14;

per cases ( p = q or p <> q ) ;

suppose p = q ; :: thesis: [b₁,b₂] in IT1

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

end;

suppose p <> q ; :: thesis: [b₁,b₂] in IT1

then ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) by A35, A38, A39;
hence [a,b] in IT1 by A34, A39; :: thesis: verum

end;

end;

end;

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