let X be set ; :: thesis:
let S be non empty Subset-Family of X; :: thesis:
assume A1: for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B ; :: thesis:
assume A2: for C, D being Element of S st D c= C holds
ex P being finite Subset of S st P is a_partition of C \ D ; :: thesis:
let A be Element of S; :: thesis:
let Q be finite Subset of S; :: thesis:
assume that
A3: not A is empty and
A4: union Q c= A and
A5: Q is a_partition of union Q ; :: thesis:
consider qq being FinSequence such that
A6: Q = rng qq by FINSEQ_1:52;
A7: for i being set st i in dom qq holds
qq . i <> {}

let i be set ; :: thesis:
assume i in dom qq ; :: thesis:
then qq . i in Q by A6, FUNCT_1:def 3;
hence qq . i <> {} by A5; :: thesis:

end;

per cases ;

suppose A8: qq = {} ; :: thesis:

then A9: Q = {} by A6;
A10: {A} is finite Subset of S by SUBSET_1:33;
A11: {A} is a_partition of A by A3, EQREL_1:39;
A12: union {A} misses union Q

proof

union Q = {} by A8, A6, ZFMISC_1:2;
hence union {A} misses union Q ; :: thesis:

end;

{} \/ {A} = {A} ;
hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A9, A10, A11, A12; :: thesis:

end;

suppose A13: qq <> {} ; :: thesis:

defpred S₁[ Nat] means for n being Nat st $1 = n & 1 <= n & n <= len qq holds
ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A );
A14: S₁[1]

proof

let n be Nat; :: thesis:
assume A15: ( n = 1 & 1 <= n & n <= len qq ) ; :: thesis:
A16: 1 in Seg (len qq) by A15;
then A17: 1 in dom qq by FINSEQ_1:def 3;
then A18: rng (qq | (Seg 1)) = {(qq . 1)} by FINSEQ_1:2, FUNCT_1:98;
A19: qq . 1 c= A

proof

qq . 1 in Q by A6, A17, FUNCT_1:def 3;
then qq . 1 c= union Q by ZFMISC_1:74;
hence qq . 1 c= A by A4, XBOOLE_1:1; :: thesis:

end;

A20: qq . 1 is Element of S

proof

1 in dom qq by A16, FINSEQ_1:def 3;
then qq . 1 in rng qq by FUNCT_1:def 3;
hence qq . 1 is Element of S by A6; :: thesis:

end;

then consider PP being finite Subset of S such that
A21: PP is a_partition of A \ (qq . 1) by A2, A19;
A21a: union PP misses qq . 1

proof

union PP = A \ (qq . 1) by A21, EQREL_1:def 4;
hence union PP misses qq . 1 by XBOOLE_1:79; :: thesis:

end;

{(qq . 1)} \/ PP is a_partition of A by A17, A7, A19, A20, A21, Lem5;
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A15, A18, A21a; :: thesis:

end;

A23: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis:
assume that
A24: 1 <= j and
A25: S₁[j] ; :: thesis:
for n being Nat st j + 1 = n & 1 <= n & n <= len qq holds
ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )

proof

let n be Nat; :: thesis:
assume that
A26: j + 1 = n and
A27: 1 <= n and
A28: n <= len qq ; :: thesis:

per cases ;

suppose j <= len qq ; :: thesis:

then consider R1 being finite Subset of S such that
A29: union R1 misses union (rng (qq | (Seg j))) and
A30: (rng (qq | (Seg j))) \/ R1 is a_partition of A by A24, A25;
A31: n in Seg (len qq) by A27, A28;
then A32: j + 1 in dom qq by A26, FINSEQ_1:def 3;
Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;
then qq | (Seg (j + 1)) = (qq | (Seg j)) \/ (qq | {(j + 1)}) by RELAT_1:78;
then A33: rng (qq | (Seg (j + 1))) = (rng (qq | (Seg j))) \/ (rng (qq | {(j + 1)})) by RELAT_1:12;
then A34: rng (qq | (Seg (j + 1))) = (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A32, FUNCT_1:98;

per cases ;

suppose qq . (j + 1) in rng (qq | (Seg j)) ; :: thesis:

then (rng (qq | (Seg j))) \/ {(qq . (j + 1))} = rng (qq | (Seg j)) by ZFMISC_1:31, XBOOLE_1:12;
then rng (qq | (Seg (j + 1))) = rng (qq | (Seg j)) by A33, A32, FUNCT_1:98;
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A26, A29, A30; :: thesis:

end;

suppose A35: not qq . (j + 1) in rng (qq | (Seg j)) ; :: thesis:

A36: qq . (j + 1) misses union (rng (qq | (Seg j)))

proof

assume not (qq . (j + 1)) /\ (union (rng (qq | (Seg j)))) = {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x0 being object such that
A37: x0 in (qq . (j + 1)) /\ (union (rng (qq | (Seg j)))) by XBOOLE_0:def 1;
( x0 in qq . (j + 1) & x0 in Union (qq | (Seg j)) ) by A37, XBOOLE_0:def 4;
then consider y0 being set such that
A38: ( x0 in y0 & y0 in rng (qq | (Seg j)) ) by TARSKI:def 4;
consider j0 being object such that
A39: j0 in dom (qq | (Seg j)) and
A40: y0 = (qq | (Seg j)) . j0 by A38, FUNCT_1:def 3;
( x0 in qq . j0 & x0 in qq . (j + 1) ) by A37, XBOOLE_0:def 4, A38, A40, A39, FUNCT_1:47;
then A41: x0 in (qq . j0) /\ (qq . (j + 1)) by XBOOLE_0:def 4;
dom (qq | (Seg j)) c= dom qq by RELAT_1:60;
then ( j0 in dom qq & j + 1 in dom qq ) by A39, A31, A26, FINSEQ_1:def 3;
then ( qq . j0 in Q & qq . (j + 1) in Q ) by A6, FUNCT_1:def 3;
then qq . j0 = qq . (j + 1) by A5, A41, XBOOLE_0:def 7, EQREL_1:def 4;
hence contradiction by A35, A38, A40, A39, FUNCT_1:47; :: thesis:

end;

A42: qq . (j + 1) in Q by A32, A6, FUNCT_1:def 3;
then A43: qq . (j + 1) c= union Q by ZFMISC_1:74;
then A44: qq . (j + 1) c= A by A4, XBOOLE_1:1;
consider RA being finite Subset of S such that
A45: RA is a_partition of A \ (qq . (j + 1)) by A42, A43, A4, XBOOLE_1:1, A2;
A46: for x being set st x in [:R1,RA:] holds
ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 )

proof

let x be set ; :: thesis:
assume x in [:R1,RA:] ; :: thesis:
then consider x1, x2 being object such that
A47: ( x1 in R1 & x2 in RA & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
consider px being finite Subset of S such that
A48: px is a_partition of x1 /\ x2 by A47, A1;
thus ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 ) by A47, A48; :: thesis:

end;

defpred S₂[ object , object ] means ( $1 in [:R1,RA:] & ex x1, x2 being set ex px being finite Subset of S st
( $1 = [x1,x2] & x1 in R1 & x2 in RA & $2 = px & $2 is a_partition of x1 /\ x2 ) );
set XA = { x where x is finite Subset of S : verum } ;
A49: for x being object st x in [:R1,RA:] holds
ex y being object st
( y in { x where x is finite Subset of S : verum } & S₂[x,y] )

proof

let x be object ; :: thesis:
assume A50: x in [:R1,RA:] ; :: thesis:
then consider x1, x2 being set , px being finite Subset of S such that
A51: x = [x1,x2] and
A52: ( x1 in R1 & x2 in RA ) and
A53: px is a_partition of x1 /\ x2 by A46;
px in { x where x is finite Subset of S : verum } ;
hence ex y being object st
( y in { x where x is finite Subset of S : verum } & S₂[x,y] ) by A50, A51, A52, A53; :: thesis:

end;

consider h being Function such that
A55: ( dom h = [:R1,RA:] & rng h c= { x where x is finite Subset of S : verum } ) and
A56: for x being object st x in [:R1,RA:] holds
S₂[x,h . x] from FUNCT_1:sch 6(A49);
A57: Union h is finite

proof

for x being set st x in rng h holds
x is finite

proof

let x be set ; :: thesis:
assume x in rng h ; :: thesis:
then consider x0 being object such that
A58: x0 in dom h and
A59: x = h . x0 by FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
x0 = [x1,x2] and
( x1 in R1 & x2 in RA ) and
A60: x = px and
x is a_partition of x1 /\ x2 by A58, A59, A55, A56;
thus x is finite by A60; :: thesis:

end;

hence Union h is finite by A55, FINSET_1:7, FINSET_1:8; :: thesis:

end;

A61: rng h c= bool S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng h ; :: thesis:
then consider x0 being object such that
A62: x0 in dom h and
A63: x = h . x0 by FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
x0 = [x1,x2] and
( x1 in R1 & x2 in RA ) and
A64: x = px and
x is a_partition of x1 /\ x2 by A62, A63, A55, A56;
thus x in bool S by A64; :: thesis:

end;

A65: Union h c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union h ; :: thesis:
then ex x0 being set st
( x in x0 & x0 in rng h ) by TARSKI:def 4;
hence x in S by A61; :: thesis:

end;

A68: union (Union h) misses union (rng (qq | (Seg n)))

proof

(union (Union h)) /\ (union (rng (qq | (Seg (j + 1))))) c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (union (Union h)) /\ (union (rng (qq | (Seg (j + 1))))) ; :: thesis:
then A69: ( x in union (Union h) & x in union (rng (qq | (Seg (j + 1)))) ) by XBOOLE_0:def 4;
then consider x0 being set such that
A70: x in x0 and
A71: x0 in Union h by TARSKI:def 4;
consider x1 being set such that
A72: x in x1 and
A73: x1 in rng (qq | (Seg (j + 1))) by A69, TARSKI:def 4;
x0 /\ x1 = {}

proof

x0 /\ x1 c= {}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A74: u in x0 /\ x1 ; :: thesis:
then A75: ( u in x0 & u in x1 ) by XBOOLE_0:def 4;
consider x0a being set such that
A76: x0 in x0a and
A77: x0a in rng h by A71, TARSKI:def 4;
consider t being object such that
A78: t in dom h and
A79: h . t = x0a by A77, FUNCT_1:def 3;
consider ax1, ax2 being set , apx being finite Subset of S such that
t = [ax1,ax2] and
A80: ( ax1 in R1 & ax2 in RA ) and
A81: x0a = apx and
A82: x0a is a_partition of ax1 /\ ax2 by A78, A79, A55, A56;
A83: ( u in x0 & x0 in apx ) by A74, XBOOLE_0:def 4, A76, A81;
( u in ax1 & ax1 in R1 ) by A83, A82, A81, A80, XBOOLE_0:def 4;
then u in union R1 by TARSKI:def 4;
then A85: not u in union (rng (qq | (Seg j))) by A29, XBOOLE_0:def 4;
( u in ax2 & ax2 in RA ) by A83, A82, A81, XBOOLE_0:def 4, A80;
then A85a: not u in qq . (j + 1) by A45, XBOOLE_0:def 5;
union (rng (qq | (Seg (j + 1)))) = union ((rng (qq | (Seg j))) \/ {(qq . (j + 1))}) by A33, A32, FUNCT_1:98;
then union (rng (qq | (Seg (j + 1)))) = (union (rng (qq | (Seg j)))) \/ (union {(qq . (j + 1))}) by ZFMISC_1:78;
then not u in union (rng (qq | (Seg (j + 1)))) by A85, XBOOLE_0:def 3, A85a;
hence u in {} by A75, A73, TARSKI:def 4; :: thesis:

end;

hence x0 /\ x1 = {} ; :: thesis:

end;

hence x in {} by A70, A72, XBOOLE_0:def 4; :: thesis:

end;

hence union (Union h) misses union (rng (qq | (Seg n))) by A26; :: thesis:

end;

(rng (qq | (Seg n))) \/ (Union h) is a_partition of A

proof

A87: (rng (qq | (Seg n))) \/ (Union h) c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A88: x in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis:
A89: ( x in rng (qq | (Seg n)) implies x in bool A )

proof

assume x in rng (qq | (Seg n)) ; :: thesis:
then x in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A26, A33, A32, FUNCT_1:98;
then ( x in rng (qq | (Seg j)) or x in {(qq . (j + 1))} ) by XBOOLE_0:def 3;
then A90: ( x in rng (qq | (Seg j)) or x = qq . (j + 1) ) by TARSKI:def 1;
( x in rng (qq | (Seg j)) implies x in bool A )

proof

assume x in rng (qq | (Seg j)) ; :: thesis:
then x in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
hence x in bool A by A30; :: thesis:

end;

hence x in bool A by A90, A44; :: thesis:

end;

( x in Union h implies x in bool A )

proof

assume x in Union h ; :: thesis:
then consider y being set such that
A91: x in y and
A92: y in rng h by TARSKI:def 4;
consider z being object such that
A93: z in dom h and
A94: y = h . z by A92, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
z = [x1,x2] and
A95: ( x1 in R1 & x2 in RA ) and
y = px and
A96: y is a_partition of x1 /\ x2 by A55, A56, A93, A94;
A97: x1 /\ x2 c= x2 by XBOOLE_1:17;
A \ (qq . (j + 1)) c= A by XBOOLE_1:36;
then x2 c= A by A45, A95, XBOOLE_1:1;
then x1 /\ x2 c= A by A97, XBOOLE_1:1;
then bool (x1 /\ x2) c= bool A by ZFMISC_1:67;
then y c= bool A by A96, XBOOLE_1:1;
hence x in bool A by A91; :: thesis:

end;

hence x in bool A by A88, A89, XBOOLE_0:def 3; :: thesis:

end;

A98: union ((rng (qq | (Seg n))) \/ (Union h)) = A

proof

A99: union ((rng (qq | (Seg n))) \/ (Union h)) c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union ((rng (qq | (Seg n))) \/ (Union h)) ; :: thesis:
then consider y being set such that
A100: x in y and
A101: y in (rng (qq | (Seg n))) \/ (Union h) by TARSKI:def 4;
thus x in A by A100, A87, A101; :: thesis:

end;

A c= union ((rng (qq | (Seg n))) \/ (Union h))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then x in union ((rng (qq | (Seg j))) \/ R1) by A30, EQREL_1:def 4;
then A102: x in (union (rng (qq | (Seg j)))) \/ (union R1) by ZFMISC_1:78;
A103: ( x in union (rng (qq | (Seg j))) implies x in union (rng (qq | (Seg (j + 1)))) )

proof

assume A104: x in union (rng (qq | (Seg j))) ; :: thesis:
union (rng (qq | (Seg j))) c= union (rng (qq | (Seg (j + 1)))) by ZFMISC_1:77, A33, XBOOLE_1:7;
hence x in union (rng (qq | (Seg (j + 1)))) by A104; :: thesis:

end;

( not x in union R1 or x in union (Union h) or x in union (rng (qq | (Seg (j + 1)))) )

proof

assume A105: x in union R1 ; :: thesis:
union R1 c= (union R1) \/ (union (rng (qq | (Seg j)))) by XBOOLE_1:7;
then union R1 c= union (R1 \/ (rng (qq | (Seg j)))) by ZFMISC_1:78;
then A106: union R1 c= A by A30, EQREL_1:def 4;
A107: ( x in qq . (j + 1) implies x in union (rng (qq | (Seg (j + 1)))) )

proof

assume A108: x in qq . (j + 1) ; :: thesis:
union (rng (qq | (Seg (j + 1)))) = union ((rng (qq | (Seg j))) \/ {(qq . (j + 1))}) by A33, A32, FUNCT_1:98;
then A108aa: union (rng (qq | (Seg (j + 1)))) = (union (rng (qq | (Seg j)))) \/ (union {(qq . (j + 1))}) by ZFMISC_1:78;
qq . (j + 1) c= union (rng (qq | (Seg (j + 1)))) by A108aa, XBOOLE_1:7;
hence x in union (rng (qq | (Seg (j + 1)))) by A108; :: thesis:

end;

( not x in qq . (j + 1) implies x in union (Union h) )

proof

assume not x in qq . (j + 1) ; :: thesis:
then x in A \ (qq . (j + 1)) by A105, A106, XBOOLE_0:def 5;
then x in union RA by A45, EQREL_1:def 4;
then consider y being set such that
A109: x in y and
A110: y in RA by TARSKI:def 4;
consider z being set such that
A111: x in z and
A112: z in R1 by A105, TARSKI:def 4;
consider t being set such that
A113: t = [z,y] ;
A114: [z,y] in [:R1,RA:] by A110, A112, ZFMISC_1:def 2;
A115: [z,y] in dom h by A110, A112, ZFMISC_1:def 2, A55;
consider x1, x2 being set , px being finite Subset of S such that
A116: t = [x1,x2] and
( x1 in R1 & x2 in RA ) and
h . t = px and
A117: h . t is a_partition of x1 /\ x2 by A113, A56, A114;
A118: ( z = x1 & y = x2 ) by A113, A116, XTUPLE_0:1;
x in z /\ y by A109, A111, XBOOLE_0:def 4;
then A119: x in union (h . t) by A117, A118, EQREL_1:def 4;
h . t in rng h by A113, A115, FUNCT_1:def 3;
then union (h . t) c= union (union (rng h)) by ZFMISC_1:74, ZFMISC_1:77;
hence x in union (Union h) by A119; :: thesis:

end;

hence ( x in union (Union h) or x in union (rng (qq | (Seg (j + 1)))) ) by A107; :: thesis:

end;

then x in (union (rng (qq | (Seg (j + 1))))) \/ (union (Union h)) by A102, A103, XBOOLE_0:def 3;
hence x in union ((rng (qq | (Seg n))) \/ (Union h)) by ZFMISC_1:78, A26; :: thesis:

end;

hence union ((rng (qq | (Seg n))) \/ (Union h)) = A by A99; :: thesis:

end;

for a being Subset of A st a in (rng (qq | (Seg n))) \/ (Union h) holds
( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) )

proof

let a be Subset of A; :: thesis:
assume A120: a in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis:
A121: ( a in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} or a in Union h ) by A34, A120, A26, XBOOLE_0:def 3;
A122: a <> {}

proof

A123: ( a in rng (qq | (Seg (j + 1))) implies a <> {} )

proof

assume a in rng (qq | (Seg (j + 1))) ; :: thesis:
then A124: a in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A33, A32, FUNCT_1:98;
A125: ( a in rng (qq | (Seg j)) implies a <> {} )

proof

assume A126: a in rng (qq | (Seg j)) ; :: thesis:
rng (qq | (Seg j)) c= (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7;
hence a <> {} by A126, A30; :: thesis:

end;

( a in {(qq . (j + 1))} implies a <> {} )

proof

assume a in {(qq . (j + 1))} ; :: thesis:
then a = qq . (j + 1) by TARSKI:def 1;
hence a <> {} by A7, A32; :: thesis:

end;

hence a <> {} by A124, A125, XBOOLE_0:def 3; :: thesis:

end;

( a in Union h implies a <> {} )

proof

assume a in Union h ; :: thesis:
then consider a1 being set such that
A127: a in a1 and
A128: a1 in rng h by TARSKI:def 4;
consider a2 being object such that
A129: a2 in dom h and
A130: a1 = h . a2 by A128, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
( a2 = [x1,x2] & x1 in R1 & x2 in RA & a1 = px ) and
A131: a1 is a_partition of x1 /\ x2 by A129, A55, A56, A130;
thus a <> {} by A127, A131; :: thesis:

end;

hence a <> {} by A120, A26, XBOOLE_0:def 3, A123; :: thesis:

end;

for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b )

proof

let b be Subset of A; :: thesis:
assume b in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis:
then ( b in rng (qq | (Seg (j + 1))) or b in Union h ) by A26, XBOOLE_0:def 3;
then A132: ( b in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} or b in Union h ) by A33, A32, FUNCT_1:98;
A133: ( not b in rng (qq | (Seg j)) or a = b or a misses b )

proof

assume A134: b in rng (qq | (Seg j)) ; :: thesis:
then A135: b in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
A136: ( not a in rng (qq | (Seg j)) or a = b or a misses b )

proof

assume a in rng (qq | (Seg j)) ; :: thesis:
then a in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
hence ( a = b or a misses b ) by A135, A30, EQREL_1:def 4; :: thesis:

end;

A137: ( not a in {(qq . (j + 1))} or a = b or a misses b )

proof

assume a in {(qq . (j + 1))} ; :: thesis:
then a misses Union (qq | (Seg j)) by A36, TARSKI:def 1;
hence ( a = b or a misses b ) by XBOOLE_1:63, A134, ZFMISC_1:74; :: thesis:

end;

( not a in Union h or a = b or a misses b )

proof

assume a in Union h ; :: thesis:
then A138: a c= union (Union h) by ZFMISC_1:74;
rng (qq | (Seg j)) c= rng (qq | (Seg (j + 1))) by A33, XBOOLE_1:7;
then b c= union (rng (qq | (Seg n))) by A134, A26, ZFMISC_1:74;
hence ( a = b or a misses b ) by A138, A68, XBOOLE_1:64; :: thesis:

end;

hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A136, A137; :: thesis:

end;

A139: ( not b in {(qq . (j + 1))} or a = b or a misses b )

proof

assume A140: b in {(qq . (j + 1))} ; :: thesis:
A141: ( not a in rng (qq | (Seg j)) or a = b or a misses b )

proof

assume A142: a in rng (qq | (Seg j)) ; :: thesis:
b misses Union (qq | (Seg j)) by A140, TARSKI:def 1, A36;
hence ( a = b or a misses b ) by A142, ZFMISC_1:74, XBOOLE_1:63; :: thesis:

end;

A143: ( not a in {(qq . (j + 1))} or a = b or a misses b )

proof

assume a in {(qq . (j + 1))} ; :: thesis:
then ( a = qq . (j + 1) & b = qq . (j + 1) ) by A140, TARSKI:def 1;
hence ( a = b or a misses b ) ; :: thesis:

end;

( not a in Union h or a = b or a misses b )

proof

assume a in Union h ; :: thesis:
then consider a1 being set such that
A144: a in a1 and
A145: a1 in rng h by TARSKI:def 4;
consider t being object such that
A146: t in dom h and
A147: a1 = h . t by A145, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
t = [x1,x2] and
A148: ( x1 in R1 & x2 in RA ) and
a1 = px and
A149: a1 is a_partition of x1 /\ x2 by A146, A147, A55, A56;
x1 /\ x2 c= x2 by XBOOLE_1:17;
then x1 /\ x2 c= A \ (qq . (j + 1)) by A45, A148, XBOOLE_1:1;
then A150: bool (x1 /\ x2) c= bool (A \ (qq . (j + 1))) by ZFMISC_1:67;
A151: a1 c= bool (A \ (qq . (j + 1))) by A149, A150, XBOOLE_1:1;
b = qq . (j + 1) by A140, TARSKI:def 1;
hence ( a = b or a misses b ) by A151, A144, XBOOLE_1:63, XBOOLE_1:79; :: thesis:

end;

hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A141, A143; :: thesis:

end;

( not b in Union h or a = b or a misses b )

proof

assume A152: b in Union h ; :: thesis:
A153: ( not a in rng (qq | (Seg j)) or a = b or a misses b )

proof

assume A154: a in rng (qq | (Seg j)) ; :: thesis:
A155: b c= union (Union h) by A152, ZFMISC_1:74;
rng (qq | (Seg j)) c= rng (qq | (Seg (j + 1))) by A33, XBOOLE_1:7;
then a c= union (rng (qq | (Seg n))) by A154, A26, ZFMISC_1:74;
hence ( a = b or a misses b ) by A155, A68, XBOOLE_1:64; :: thesis:

end;

A156: ( not a in {(qq . (j + 1))} or a = b or a misses b )

proof

assume a in {(qq . (j + 1))} ; :: thesis:
then A157: a = qq . (j + 1) by TARSKI:def 1;
consider b1 being set such that
A158: b in b1 and
A159: b1 in rng h by A152, TARSKI:def 4;
consider tb being object such that
A160: tb in dom h and
A161: b1 = h . tb by A159, FUNCT_1:def 3;
consider bx1, bx2 being set , bpx being finite Subset of S such that
tb = [bx1,bx2] and
A162: ( bx1 in R1 & bx2 in RA ) and
b1 = bpx and
A163: b1 is a_partition of bx1 /\ bx2 by A160, A161, A55, A56;
A164: bool (bx1 /\ bx2) c= bool bx2 by XBOOLE_1:17, ZFMISC_1:67;
b1 c= bool bx2 by A163, A164, XBOOLE_1:1;
then b c= A \ (qq . (j + 1)) by A45, A162, A158, XBOOLE_1:1;
hence ( a = b or a misses b ) by XBOOLE_1:79, A157, XBOOLE_1:63; :: thesis:

end;

( not a in Union h or a = b or a misses b )

proof

assume a in Union h ; :: thesis:
then consider a1 being set such that
A166: a in a1 and
A167: a1 in rng h by TARSKI:def 4;
consider t being object such that
A168: t in dom h and
A169: a1 = h . t by A167, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
A170: t = [x1,x2] and
A171: ( x1 in R1 & x2 in RA ) and
a1 = px and
A172: a1 is a_partition of x1 /\ x2 by A168, A169, A55, A56;
consider b1 being set such that
A173: b in b1 and
A174: b1 in rng h by A152, TARSKI:def 4;
consider tb being object such that
A175: tb in dom h and
A176: b1 = h . tb by A174, FUNCT_1:def 3;
consider bx1, bx2 being set , bpx being finite Subset of S such that
A177: tb = [bx1,bx2] and
A178: ( bx1 in R1 & bx2 in RA ) and
b1 = bpx and
A179: b1 is a_partition of bx1 /\ bx2 by A175, A176, A55, A56;
A180: ( not x1 = bx1 & not x2 = bx2 & not a = b implies a misses b )

proof

assume A181: ( not x1 = bx1 & not x2 = bx2 ) ; :: thesis:
A182: ( x1 in (rng (qq | (Seg j))) \/ R1 & bx1 in (rng (qq | (Seg j))) \/ R1 ) by A171, A178, XBOOLE_1:7, TARSKI:def 3;
A183: ( bool (x1 /\ x2) c= bool x1 & bool (bx1 /\ bx2) c= bool bx1 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x1 & b1 c= bool bx1 ) by A172, A179, A183, XBOOLE_1:1;
hence ( a = b or a misses b ) by A182, A181, A30, EQREL_1:def 4, A166, A173, XBOOLE_1:64; :: thesis:

end;

A184: ( x1 = bx1 & not x2 = bx2 & not a = b implies a misses b )

proof

assume A185: ( x1 = bx1 & not x2 = bx2 ) ; :: thesis:
A186: ( bool (x1 /\ x2) c= bool x2 & bool (bx1 /\ bx2) c= bool bx2 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x2 & b1 c= bool bx2 ) by A172, A179, A186, XBOOLE_1:1;
hence ( a = b or a misses b ) by A166, A173, A185, A171, A178, A45, EQREL_1:def 4, XBOOLE_1:64; :: thesis:

end;

( not x1 = bx1 & x2 = bx2 & not a = b implies a misses b )

proof

assume A187: ( not x1 = bx1 & x2 = bx2 ) ; :: thesis:
A188: ( x1 in (rng (qq | (Seg j))) \/ R1 & bx1 in (rng (qq | (Seg j))) \/ R1 ) by A171, A178, XBOOLE_1:7, TARSKI:def 3;
A189: ( bool (x1 /\ x2) c= bool x1 & bool (bx1 /\ bx2) c= bool bx1 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x1 & b1 c= bool bx1 ) by A172, A179, A189, XBOOLE_1:1;
hence ( a = b or a misses b ) by A166, A173, XBOOLE_1:64, A188, A187, A30, EQREL_1:def 4; :: thesis:

end;

hence ( a = b or a misses b ) by A169, A176, A170, A177, A166, A173, A172, EQREL_1:def 4, A180, A184; :: thesis:

end;

hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A153, A156; :: thesis:

end;

hence ( a = b or a misses b ) by A132, XBOOLE_0:def 3, A133, A139; :: thesis:

end;

hence ( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) ) by A122; :: thesis:

end;

hence (rng (qq | (Seg n))) \/ (Union h) is a_partition of A by A87, A98, EQREL_1:def 4; :: thesis:

end;

hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A65, A57, A68; :: thesis:

end;

suppose not j <= len qq ; :: thesis:

hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A28, A26, XREAL_1:39; :: thesis:

end;

hence S₁[j + 1] ; :: thesis:

end;

A190: for i being Nat st 1 <= i holds
S₁[i] from NAT_1:sch 8(A14, A23);
A191: ( len qq is Nat & 1 <= len qq ) by A13, FINSEQ_1:20;
consider R being finite Subset of S such that
A192: union R misses union (rng (qq | (Seg (len qq)))) and
A193: (rng (qq | (Seg (len qq)))) \/ R is a_partition of A by A190, A191;
rng (qq | (Seg (len qq))) = Q

proof

rng (qq | (Seg (len qq))) = rng (qq | (dom qq)) by FINSEQ_1:def 3
.= rng qq ;
hence rng (qq | (Seg (len qq))) = Q by A6; :: thesis:

end;

hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A193, A192; :: thesis:

end;