A1: i + 1 = (i + 1) -' 0 by NAT_D:40;
defpred S1[ object , object ] means ex p, q being bag of n st
( $1 = p & $2 = q & ( ( (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 ) ) );
consider BO being Relation of (Bags n),(Bags n) such that
A2: for x, y being object holds
( [x,y] in BO iff ( x in Bags n & y in Bags n & S1[x,y] ) ) from RELSET_1:sch 1();
now :: thesis: for x being object st x in Bags n holds
[x,x] in BO
let x be object ; :: thesis: ( x in Bags n implies [x,x] in BO )
assume A3: x in Bags n ; :: thesis: [x,x] in BO
reconsider x9 = x as bag of n by A3;
A4: (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut x9 ;
((i + 1),n) -cut x9 in Bags (n -' (i + 1)) by PRE_POLY:def 12;
then [(((i + 1),n) -cut x9),(((i + 1),n) -cut x9)] in o2 by ORDERS_1:3;
hence [x,x] in BO by A2, A3, A4; :: thesis: verum
end;
then A5: BO is_reflexive_in Bags n ;
now :: thesis: for x, y being object st x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO holds
x = y
let x, y be object ; :: thesis: ( x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO implies b1 = b2 )
assume that
x in Bags n and
y in Bags n and
A6: [x,y] in BO and
A7: [y,x] in BO ; :: thesis: b1 = b2
consider p, q being bag of n such that
A8: x = p and
A9: y = q and
A10: ( ( (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 A2, A6;
A11: ex q9, p9 being bag of n st
( y = q9 & x = p9 & ( ( (0,(i + 1)) -cut q9 <> (0,(i + 1)) -cut p9 & [((0,(i + 1)) -cut q9),((0,(i + 1)) -cut p9)] in o1 ) or ( (0,(i + 1)) -cut q9 = (0,(i + 1)) -cut p9 & [(((i + 1),n) -cut q9),(((i + 1),n) -cut p9)] in o2 ) ) ) by A2, A7;
set CUTP1 = (0,(i + 1)) -cut p;
set CUTP2 = ((i + 1),n) -cut p;
set CUTQ1 = (0,(i + 1)) -cut q;
set CUTQ2 = ((i + 1),n) -cut q;
A12: (0,(i + 1)) -cut p in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A13: (0,(i + 1)) -cut q in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A14: ((i + 1),n) -cut p in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A15: ((i + 1),n) -cut q in Bags (n -' (i + 1)) by PRE_POLY:def 12;
per cases ( ( (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 A10;
suppose A16: ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) ; :: thesis: b1 = b2
now :: thesis: x = y
per cases ( ( (0,(i + 1)) -cut q <> (0,(i + 1)) -cut p & [((0,(i + 1)) -cut q),((0,(i + 1)) -cut p)] in o1 ) or ( (0,(i + 1)) -cut q = (0,(i + 1)) -cut p & [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 ) ) by A8, A9, A11;
suppose ( (0,(i + 1)) -cut q <> (0,(i + 1)) -cut p & [((0,(i + 1)) -cut q),((0,(i + 1)) -cut p)] in o1 ) ; :: thesis: x = y
hence x = y by A1, A12, A13, A16, ORDERS_1:4; :: thesis: verum
end;
suppose ( (0,(i + 1)) -cut q = (0,(i + 1)) -cut p & [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 ) ; :: thesis: x = y
hence x = y by A16; :: thesis: verum
end;
end;
end;
hence x = y ; :: thesis: verum
end;
suppose A17: ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ; :: thesis: b1 = b2
now :: thesis: x = y
per cases ( ( (0,(i + 1)) -cut q <> (0,(i + 1)) -cut p & [((0,(i + 1)) -cut q),((0,(i + 1)) -cut p)] in o1 ) or ( (0,(i + 1)) -cut q = (0,(i + 1)) -cut p & [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 ) ) by A8, A9, A11;
suppose ( (0,(i + 1)) -cut q <> (0,(i + 1)) -cut p & [((0,(i + 1)) -cut q),((0,(i + 1)) -cut p)] in o1 ) ; :: thesis: x = y
hence x = y by A17; :: thesis: verum
end;
suppose ( (0,(i + 1)) -cut q = (0,(i + 1)) -cut p & [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 ) ; :: thesis: x = y
then ((i + 1),n) -cut q = ((i + 1),n) -cut p by A14, A15, A17, ORDERS_1:4;
hence x = y by A8, A9, A17, Th4; :: thesis: verum
end;
end;
end;
hence x = y ; :: thesis: verum
end;
end;
end;
then A18: BO is_antisymmetric_in Bags n ;
now :: thesis: for x, y, z being object st x in Bags n & y in Bags n & z in Bags n & [x,y] in BO & [y,z] in BO holds
[x,z] in BO
let x, y, z be object ; :: thesis: ( x in Bags n & y in Bags n & z in Bags n & [x,y] in BO & [y,z] in BO implies [b1,b3] in BO )
assume that
A19: x in Bags n and
y in Bags n and
A20: z in Bags n and
A21: [x,y] in BO and
A22: [y,z] in BO ; :: thesis: [b1,b3] in BO
consider x9, y9 being bag of n such that
A23: x9 = x and
A24: y9 = y and
A25: ( ( (0,(i + 1)) -cut x9 <> (0,(i + 1)) -cut y9 & [((0,(i + 1)) -cut x9),((0,(i + 1)) -cut y9)] in o1 ) or ( (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut y9 & [(((i + 1),n) -cut x9),(((i + 1),n) -cut y9)] in o2 ) ) by A2, A21;
consider y99, z9 being bag of n such that
A26: y99 = y and
A27: z9 = z and
A28: ( ( (0,(i + 1)) -cut y99 <> (0,(i + 1)) -cut z9 & [((0,(i + 1)) -cut y99),((0,(i + 1)) -cut z9)] in o1 ) or ( (0,(i + 1)) -cut y99 = (0,(i + 1)) -cut z9 & [(((i + 1),n) -cut y99),(((i + 1),n) -cut z9)] in o2 ) ) by A2, A22;
set CUTX1 = (0,(i + 1)) -cut x9;
set CUTX2 = ((i + 1),n) -cut x9;
set CUTY1 = (0,(i + 1)) -cut y9;
set CUTY2 = ((i + 1),n) -cut y9;
set CUTZ1 = (0,(i + 1)) -cut z9;
set CUTZ2 = ((i + 1),n) -cut z9;
A29: (0,(i + 1)) -cut x9 in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A30: (0,(i + 1)) -cut y9 in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A31: (0,(i + 1)) -cut z9 in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A32: ((i + 1),n) -cut x9 in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A33: ((i + 1),n) -cut y9 in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A34: ((i + 1),n) -cut z9 in Bags (n -' (i + 1)) by PRE_POLY:def 12;
per cases ( ( (0,(i + 1)) -cut x9 <> (0,(i + 1)) -cut y9 & [((0,(i + 1)) -cut x9),((0,(i + 1)) -cut y9)] in o1 ) or ( (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut y9 & [(((i + 1),n) -cut x9),(((i + 1),n) -cut y9)] in o2 ) ) by A25;
suppose A35: ( (0,(i + 1)) -cut x9 <> (0,(i + 1)) -cut y9 & [((0,(i + 1)) -cut x9),((0,(i + 1)) -cut y9)] in o1 ) ; :: thesis: [b1,b3] in BO
now :: thesis: [x,z] in BO
per cases ( ( (0,(i + 1)) -cut y9 <> (0,(i + 1)) -cut z9 & [((0,(i + 1)) -cut y9),((0,(i + 1)) -cut z9)] in o1 ) or ( (0,(i + 1)) -cut y9 = (0,(i + 1)) -cut z9 & [(((i + 1),n) -cut y9),(((i + 1),n) -cut z9)] in o2 ) ) by A24, A26, A28;
suppose A36: ( (0,(i + 1)) -cut y9 <> (0,(i + 1)) -cut z9 & [((0,(i + 1)) -cut y9),((0,(i + 1)) -cut z9)] in o1 ) ; :: thesis: [x,z] in BO
then A37: [((0,(i + 1)) -cut x9),((0,(i + 1)) -cut z9)] in o1 by A1, A29, A30, A31, A35, ORDERS_1:5;
now :: thesis: [x,z] in BO
per cases ( (0,(i + 1)) -cut x9 <> (0,(i + 1)) -cut z9 or (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut z9 ) ;
suppose (0,(i + 1)) -cut x9 <> (0,(i + 1)) -cut z9 ; :: thesis: [x,z] in BO
hence [x,z] in BO by A2, A19, A20, A23, A27, A37; :: thesis: verum
end;
suppose (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut z9 ; :: thesis: [x,z] in BO
hence [x,z] in BO by A1, A29, A30, A35, A36, ORDERS_1:4; :: thesis: verum
end;
end;
end;
hence [x,z] in BO ; :: thesis: verum
end;
suppose ( (0,(i + 1)) -cut y9 = (0,(i + 1)) -cut z9 & [(((i + 1),n) -cut y9),(((i + 1),n) -cut z9)] in o2 ) ; :: thesis: [x,z] in BO
hence [x,z] in BO by A2, A19, A20, A23, A27, A35; :: thesis: verum
end;
end;
end;
hence [x,z] in BO ; :: thesis: verum
end;
suppose A38: ( (0,(i + 1)) -cut x9 = (0,(i + 1)) -cut y9 & [(((i + 1),n) -cut x9),(((i + 1),n) -cut y9)] in o2 ) ; :: thesis: [b1,b3] in BO
now :: thesis: [x,z] in BO
per cases ( ( (0,(i + 1)) -cut y9 <> (0,(i + 1)) -cut z9 & [((0,(i + 1)) -cut y9),((0,(i + 1)) -cut z9)] in o1 ) or ( (0,(i + 1)) -cut y9 = (0,(i + 1)) -cut z9 & [(((i + 1),n) -cut y9),(((i + 1),n) -cut z9)] in o2 ) ) by A24, A26, A28;
suppose ( (0,(i + 1)) -cut y9 <> (0,(i + 1)) -cut z9 & [((0,(i + 1)) -cut y9),((0,(i + 1)) -cut z9)] in o1 ) ; :: thesis: [x,z] in BO
hence [x,z] in BO by A2, A19, A20, A23, A27, A38; :: thesis: verum
end;
suppose A39: ( (0,(i + 1)) -cut y9 = (0,(i + 1)) -cut z9 & [(((i + 1),n) -cut y9),(((i + 1),n) -cut z9)] in o2 ) ; :: thesis: [x,z] in BO
then [(((i + 1),n) -cut x9),(((i + 1),n) -cut z9)] in o2 by A32, A33, A34, A38, ORDERS_1:5;
hence [x,z] in BO by A2, A19, A20, A23, A27, A38, A39; :: thesis: verum
end;
end;
end;
hence [x,z] in BO ; :: thesis: verum
end;
end;
end;
then A40: BO is_transitive_in Bags n ;
A41: dom BO = Bags n by A5, ORDERS_1:13;
field BO = Bags n by A5, ORDERS_1:13;
then reconsider BO = BO as TermOrder of n by A5, A18, A40, A41, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take BO ; :: thesis: for p, q being bag of n holds
( [p,q] in BO 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 ) ) )
let p, q be bag of n; :: thesis: ( [p,q] in BO 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 ) ) )
hereby :: thesis: ( ( ( (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 [p,q] in BO )
assume [p,q] in BO ; :: thesis: ( ( (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 ) )
then ex p9, q9 being bag of n st
( p9 = p & q9 = q & ( ( (0,(i + 1)) -cut p9 <> (0,(i + 1)) -cut q9 & [((0,(i + 1)) -cut p9),((0,(i + 1)) -cut q9)] in o1 ) or ( (0,(i + 1)) -cut p9 = (0,(i + 1)) -cut q9 & [(((i + 1),n) -cut p9),(((i + 1),n) -cut q9)] in o2 ) ) ) by A2;
hence ( ( (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: verum
end;
assume A42: ( ( (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: [p,q] in BO
A43: p in Bags n by PRE_POLY:def 12;
q in Bags n by PRE_POLY:def 12;
hence [p,q] in BO by A2, A42, A43; :: thesis: verum