let IT1, IT2 be TermOrder of n; :: thesis: ( ( for p, q being bag of n 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 n 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

A49: for p, q being bag of n 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

A50: for p, q being bag of n 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

( [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 n 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

A49: for p, q being bag of n 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

A50: for p, q being bag of n 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 :: 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 [b_{1},b_{2}] in IT1 ) )

_{1},b_{2}] in IT1

then consider p, q being object such that

A56: [a,b] = [p,q] and

A57: p in Bags n and

A58: q in Bags n by RELSET_1:2;

reconsider p = p, q = q as bag of n by A57, A58;

end;hereby :: thesis: ( [a,b] in IT2 implies [b_{1},b_{2}] in IT1 )

assume A55:
[a,b] in IT2
; :: thesis: [bassume A51:
[a,b] in IT1
; :: thesis: [a,b] in IT2

then consider p, q being object such that

A52: [a,b] = [p,q] and

A53: p in Bags n and

A54: q in Bags n by RELSET_1:2;

reconsider p = p, q = q as bag of n by A53, A54;

end;then consider p, q being object such that

A52: [a,b] = [p,q] and

A53: p in Bags n and

A54: q in Bags n by RELSET_1:2;

reconsider p = p, q = q as bag of n by A53, A54;

then consider p, q being object such that

A56: [a,b] = [p,q] and

A57: p in Bags n and

A58: q in Bags n by RELSET_1:2;

reconsider p = p, q = q as bag of n by A57, A58;