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 for x being object st x in Bags n holds
[x,x] in BOlet x be
object ;
( x in Bags n implies [x,x] in BO )assume A3:
x in Bags n
;
[x,x] in BOreconsider 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;
verum end;
then A5:
BO is_reflexive_in Bags n
;
now for x, y being object st x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO holds
x = ylet x,
y be
object ;
( 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
;
b1 = b2consider 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 )
;
b1 = b2now x = yper 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;
end; end; hence
x = y
;
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 )
;
b1 = b2now x = yper 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;
end; end; hence
x = y
;
verum end; end; end;
then A18:
BO is_antisymmetric_in Bags n
;
now 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 BOlet x,
y,
z be
object ;
( 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
;
[b1,b3] in BOconsider 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 )
;
[b1,b3] in BOnow [x,z] in BOper 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;
end; end; hence
[x,z] in BO
;
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 )
;
[b1,b3] in BOnow [x,z] in BOper 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 A39:
( (
0,
(i + 1))
-cut y9 = (
0,
(i + 1))
-cut z9 &
[(((i + 1),n) -cut y9),(((i + 1),n) -cut z9)] in o2 )
;
[x,z] in BOthen
[(((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;
verum end; end; end; hence
[x,z] in BO
;
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
; 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; ( [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 ( ( ( (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
;
( ( (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 ) )
;
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 ) )
; [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; verum