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 , 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 x' = x as bag of n by A3, PRE_POLY:def 12;
A4: 0 ,(i + 1) -cut x' = 0 ,(i + 1) -cut x' ;
(i + 1),n -cut x' in Bags (n -' (i + 1)) by PRE_POLY:def 12;
then [((i + 1),n -cut x'),((i + 1),n -cut x')] 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 q', p' being bag of n st
( y = q' & x = p' & ( ( 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 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 x', y' being bag of n such that
A23: x' = x and
A24: y' = y and
A25: ( ( 0 ,(i + 1) -cut x' <> 0 ,(i + 1) -cut y' & [(0 ,(i + 1) -cut x'),(0 ,(i + 1) -cut y')] in o1 ) or ( 0 ,(i + 1) -cut x' = 0 ,(i + 1) -cut y' & [((i + 1),n -cut x'),((i + 1),n -cut y')] in o2 ) ) by A2, A21;
consider y'', z' being bag of n such that
A26: y'' = y and
A27: z' = z and
A28: ( ( 0 ,(i + 1) -cut y'' <> 0 ,(i + 1) -cut z' & [(0 ,(i + 1) -cut y''),(0 ,(i + 1) -cut z')] in o1 ) or ( 0 ,(i + 1) -cut y'' = 0 ,(i + 1) -cut z' & [((i + 1),n -cut y''),((i + 1),n -cut z')] in o2 ) ) by A2, A22;
set CUTX1 = 0 ,(i + 1) -cut x';
set CUTX2 = (i + 1),n -cut x';
set CUTY1 = 0 ,(i + 1) -cut y';
set CUTY2 = (i + 1),n -cut y';
set CUTZ1 = 0 ,(i + 1) -cut z';
set CUTZ2 = (i + 1),n -cut z';
A29: 0 ,(i + 1) -cut x' in Bags ((i + 1) -' 0 ) by PRE_POLY:def 12;
A30: 0 ,(i + 1) -cut y' in Bags ((i + 1) -' 0 ) by PRE_POLY:def 12;
A31: 0 ,(i + 1) -cut z' in Bags ((i + 1) -' 0 ) by PRE_POLY:def 12;
A32: (i + 1),n -cut x' in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A33: (i + 1),n -cut y' in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A34: (i + 1),n -cut z' in Bags (n -' (i + 1)) by PRE_POLY:def 12;
per cases ( ( 0 ,(i + 1) -cut x' <> 0 ,(i + 1) -cut y' & [(0 ,(i + 1) -cut x'),(0 ,(i + 1) -cut y')] in o1 ) or ( 0 ,(i + 1) -cut x' = 0 ,(i + 1) -cut y' & [((i + 1),n -cut x'),((i + 1),n -cut y')] in o2 ) ) by A25;
suppose A35: ( 0 ,(i + 1) -cut x' <> 0 ,(i + 1) -cut y' & [(0 ,(i + 1) -cut x'),(0 ,(i + 1) -cut y')] in o1 ) ; :: thesis: [b1,b3] in BO
now
per cases ( ( 0 ,(i + 1) -cut y' <> 0 ,(i + 1) -cut z' & [(0 ,(i + 1) -cut y'),(0 ,(i + 1) -cut z')] in o1 ) or ( 0 ,(i + 1) -cut y' = 0 ,(i + 1) -cut z' & [((i + 1),n -cut y'),((i + 1),n -cut z')] in o2 ) ) by A24, A26, A28;
suppose A36: ( 0 ,(i + 1) -cut y' <> 0 ,(i + 1) -cut z' & [(0 ,(i + 1) -cut y'),(0 ,(i + 1) -cut z')] in o1 ) ; :: thesis: [x,z] in BO
then A37: [(0 ,(i + 1) -cut x'),(0 ,(i + 1) -cut z')] in o1 by A1, A29, A30, A31, A35, ORDERS_1:14;
now
per cases ( 0 ,(i + 1) -cut x' <> 0 ,(i + 1) -cut z' or 0 ,(i + 1) -cut x' = 0 ,(i + 1) -cut z' ) ;
suppose 0 ,(i + 1) -cut x' <> 0 ,(i + 1) -cut z' ; :: 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 x' = 0 ,(i + 1) -cut z' ; :: 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 y' = 0 ,(i + 1) -cut z' & [((i + 1),n -cut y'),((i + 1),n -cut z')] 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 x' = 0 ,(i + 1) -cut y' & [((i + 1),n -cut x'),((i + 1),n -cut y')] in o2 ) ; :: thesis: [b1,b3] in BO
now
per cases ( ( 0 ,(i + 1) -cut y' <> 0 ,(i + 1) -cut z' & [(0 ,(i + 1) -cut y'),(0 ,(i + 1) -cut z')] in o1 ) or ( 0 ,(i + 1) -cut y' = 0 ,(i + 1) -cut z' & [((i + 1),n -cut y'),((i + 1),n -cut z')] in o2 ) ) by A24, A26, A28;
suppose ( 0 ,(i + 1) -cut y' <> 0 ,(i + 1) -cut z' & [(0 ,(i + 1) -cut y'),(0 ,(i + 1) -cut z')] 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 y' = 0 ,(i + 1) -cut z' & [((i + 1),n -cut y'),((i + 1),n -cut z')] in o2 ) ; :: thesis: [x,z] in BO
then [((i + 1),n -cut x'),((i + 1),n -cut z')] 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 p', q' being bag of n st
( p' = p & q' = 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 ) ) ) 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