A1: i + 1 = (i + 1) -' 0 by NAT_D:40;
defpred S1[ set , set ] 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 set holds
( [x,y] in BO iff ( x in Bags n & y in Bags n & S1[x,y] ) ) from RELSET_1:sch 1();
now
let x be set ; :: 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, PRE_POLY:def 12;
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:12;
hence [x,x] in BO by A2, A3, A4; :: thesis: verum
end;
then A5: BO is_reflexive_in Bags n by RELAT_2:def 1;
now
let x, y be set ; :: 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
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:13; :: 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
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:13;
hence x = y by A8, A9, A17, Th6; :: thesis: verum
end;
end;
end;
hence x = y ; :: thesis: verum
end;
end;
end;
then A18: BO is_antisymmetric_in Bags n by RELAT_2:def 4;
now
let x, y, z be set ; :: 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
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:14;
now
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:13; :: 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
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:14;
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 by RELAT_2:def 8;
A41: dom BO = Bags n by A5, ORDERS_1:98;
field BO = Bags n by A5, ORDERS_1:98;
then reconsider BO = BO as TermOrder of n by A5, A18, A40, A41, PARTFUN1:def 4, 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