let IT1, IT2 be TermOrder of n; :: thesis: ( ( for p, q being bag of n holds
( [p,q] in IT1 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) ) & ( for p, q being bag of n holds
( [p,q] in IT2 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) ) implies IT1 = IT2 )
assume that
A44: for p, q being bag of n holds
( [p,q] in IT1 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) and
A45: for p, q being bag of n holds
( [p,q] in IT2 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) ; :: 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 ) )

let a, b be object ; :: 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 A46: [a,b] in IT1 ; :: thesis: [a,b] in IT2
then A47: a in dom IT1 by XTUPLE_0:def 12;
b in rng IT1 by A46, XTUPLE_0:def 13;
then reconsider p = a, q = b as bag of n by A47;
( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) by A44, A46;
hence [a,b] in IT2 by A45; :: thesis: verum

end;

assume A48: [a,b] in IT2 ; :: thesis: [a,b] in IT1
then A49: a in dom IT2 by XTUPLE_0:def 12;
b in rng IT2 by A48, XTUPLE_0:def 13;
then reconsider p = a, q = b as bag of n by A49;
( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) by A45, A48;
hence [a,b] in IT1 by A44; :: thesis: verum

end;

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