let X be set ; :: thesis:
let S be cap-finite-partition-closed Subset-Family of X; :: thesis:
let A be Element of S; :: thesis:
set B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ;

T1: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } c= {}

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ; :: thesis:
then consider t0 being Element of S such that
t = t0 and
ZE2: t0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider u0 being set such that
ZE3: t0 in u0 and
ZE4: u0 in (PARTITIONS A) /\ (Fin S) by ZE2, TARSKI:def 4;
u0 in PARTITIONS A by ZE4, XBOOLE_0:def 4;
hence t in {} by H0, ZE3, A4bis, TARSKI:def 1; :: thesis:

end;

{} is Subset-Family of {} by XBOOLE_1:2;
then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as Subset-Family of {} by T1;
for a, b being Element of B st not a \ b is empty holds
ex P being finite Subset of B st P is a_partition of a \ b by T1, SUBSET_1:def 1;
then B is diff-finite-partition-closed ;
hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A by H0; :: thesis:

end;

suppose H1: not A is empty ; :: thesis:

AA: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ; :: thesis:
then consider x0 being Element of S such that
B1: x = x0 and
B2: x0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider x1 being set such that
B3: x0 in x1 and
B4: x1 in (PARTITIONS A) /\ (Fin S) by B2, TARSKI:def 4;
( x1 in PARTITIONS A & x1 in Fin S ) by B4, XBOOLE_0:def 4;
then x1 is a_partition of A by PARTIT1:def 3;
hence x in bool A by B1, B3; :: thesis:

end;

per cases } is empty or not { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ) ;

suppose U0: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ; :: thesis:

then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as Subset-Family of A by XBOOLE_1:2;
for S1, S2 being Element of B st not S1 \ S2 is empty holds
ex P being finite Subset of B st P is a_partition of S1 \ S2 by U0, SUBSET_1:def 1;
then B is diff-finite-partition-closed ;
hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A ; :: thesis:

end;

suppose not { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ; :: thesis:

then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as non empty set ;
for x, y being Element of B st y c= x holds
ex P being finite Subset of B st P is a_partition of x \ y

proof

let x, y be Element of B; :: thesis:
assume y c= x ; :: thesis:
x in B ;
then consider x0 being Element of S such that
A1: x = x0 and
A2: x0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider x1 being set such that
C1: x0 in x1 and
C2: x1 in (PARTITIONS A) /\ (Fin S) by A2, TARSKI:def 4;
y in B ;
then consider y0 being Element of S such that
A3: y = y0 and
A4: y0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider y1 being set such that
C3: y0 in y1 and
C4: y1 in (PARTITIONS A) /\ (Fin S) by A4, TARSKI:def 4;
C4A: ( x1 in PARTITIONS A & x1 in Fin S & y1 in PARTITIONS A & y1 in Fin S ) by C2, C4, XBOOLE_0:def 4;
then C5: ( x1 is a_partition of A & x1 is finite Subset of S & y1 is a_partition of A & y1 is finite Subset of S ) by PARTIT1:def 3, FINSUB_1:def 5;
reconsider A = A as non empty set by H1;
reconsider x1 = x1, y1 = y1 as a_partition of A by C4A, PARTIT1:def 3;
consider P being a_partition of A such that
D1: P is finite Subset of S and
D2: P '<' x1 '/\' y1 by C5, ThmJ1;
set P1 = { p where p is Element of P : ( p is Subset of x & p misses y ) } ;
T1: { p where p is Element of P : ( p is Subset of x & p misses y ) } is finite Subset of B

proof

T1A: { p where p is Element of P : ( p is Subset of x & p misses y ) } is finite

proof

{ p where p is Element of P : ( p is Subset of x & p misses y ) } c= P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then ex p being Element of P st
( a = p & p is Subset of x & p misses y ) ;
hence a in P ; :: thesis:

end;

hence { p where p is Element of P : ( p is Subset of x & p misses y ) } is finite by D1; :: thesis:

end;

{ p where p is Element of P : ( p is Subset of x & p misses y ) } c= B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then consider p being Element of P such that
EZ2: a = p and
p is Subset of x and
p misses y ;
( a in P & P in PARTITIONS A & P in Fin S ) by EZ2, D1, FINSUB_1:def 5, PARTIT1:def 3;
then ( a in P & P in (PARTITIONS A) /\ (Fin S) ) by XBOOLE_0:def 4;
then EZ6: a in union ((PARTITIONS A) /\ (Fin S)) by TARSKI:def 4;
a in P by EZ2;
hence a in B by D1, EZ6; :: thesis:

end;

hence { p where p is Element of P : ( p is Subset of x & p misses y ) } is finite Subset of B by T1A; :: thesis:

end;

{ p where p is Element of P : ( p is Subset of x & p misses y ) } is a_partition of x \ y

proof

Y1: { p where p is Element of P : ( p is Subset of x & p misses y ) } c= bool (x \ y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then consider p being Element of P such that
EZ7: a = p and
EZ8: p is Subset of x and
EZ9: p misses y ;
reconsider a = a as set by TARSKI:1;
a c= x \ y by EZ7, EZ8, EZ9, XBOOLE_1:86;
hence a in bool (x \ y) ; :: thesis:

end;

Y2: union { p where p is Element of P : ( p is Subset of x & p misses y ) } = x \ y

proof

thus union { p where p is Element of P : ( p is Subset of x & p misses y ) } c= x \ y :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then consider b being set such that
EZ11: a in b and
EZ12: b in { p where p is Element of P : ( p is Subset of x & p misses y ) } by TARSKI:def 4;
consider p being Element of P such that
EZ13: b = p and
EZ14: p is Subset of x and
EZ15: p misses y by EZ12;
b c= x \ y by EZ13, EZ14, EZ15, XBOOLE_1:86;
hence a in x \ y by EZ11; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume AS0: a in x \ y ; :: thesis:
then U0: a in x ;
U00: ( x in x1 & x1 is a_partition of A ) by A1, C1;
U1: a in A by U0, U00;
a in union P by U1, EQREL_1:def 4;
then consider b being set such that
U2: a in b and
U3: b in P by TARSKI:def 4;
consider u being set such that
U4: u in x1 '/\' y1 and
U5: b c= u by U3, D2, SETFAM_1:def 2;
consider xx1, yy1 being set such that
W3: ( xx1 in x1 & yy1 in y1 ) and
W4: u = xx1 /\ yy1 by U4, SETFAM_1:def 5;
UU1: b is Subset of x

proof

LI1A: ( b c= xx1 /\ yy1 & xx1 /\ yy1 c= xx1 ) by U5, W4, XBOOLE_1:17;
then LI1: b c= xx1 by XBOOLE_1:1;
xx1 = x

proof

assume not xx1 = x ; :: thesis:
then b misses x by A1, C1, W3, LI1, EQREL_1:def 4, XBOOLE_1:63;
hence contradiction by AS0, U2, XBOOLE_0:def 4; :: thesis:

end;

hence b is Subset of x by LI1A, XBOOLE_1:1; :: thesis:

end;

b misses y

proof

assume not b misses y ; :: thesis:
then consider z being object such that
WA1: z in b /\ y by XBOOLE_0:def 1;
consider v being set such that
K1: v in x1 '/\' y1 and
K2: b c= v by U3, D2, SETFAM_1:def 2;
consider xx1, yy1 being set such that
W3: ( xx1 in x1 & yy1 in y1 ) and
W4: v = xx1 /\ yy1 by K1, SETFAM_1:def 5;
LEM: not xx1 /\ yy1 = x /\ y

proof

assume xx1 /\ yy1 = x /\ y ; :: thesis:
then a in y by U2, W4, K2, XBOOLE_0:def 4;
hence contradiction by AS0, XBOOLE_0:def 5; :: thesis:

end;

( z in b /\ y & b /\ y c= (xx1 /\ yy1) /\ y ) by WA1, K2, W4, XBOOLE_1:26;
then ( z in xx1 /\ yy1 & z in y ) by XBOOLE_0:def 4;
then ( z in xx1 & z in yy1 & z in y ) by XBOOLE_0:def 4;
then AS2: z in yy1 /\ y by XBOOLE_0:def 4;
AS2A: yy1 = y by A3, C3, W3, EQREL_1:def 4, AS2, XBOOLE_0:def 7;
( a in xx1 & a in x ) by U2, K2, W4, AS0, XBOOLE_0:def 4;
then a in xx1 /\ x by XBOOLE_0:def 4;
hence contradiction by A1, C1, W3, EQREL_1:def 4, LEM, AS2A, XBOOLE_0:def 7; :: thesis:

end;

then b in { p where p is Element of P : ( p is Subset of x & p misses y ) } by UU1, U3;
hence a in union { p where p is Element of P : ( p is Subset of x & p misses y ) } by U2, TARSKI:def 4; :: thesis:

end;

for a being Subset of (x \ y) st a in { p where p is Element of P : ( p is Subset of x & p misses y ) } holds
( a <> {} & ( for b being Subset of (x \ y) holds
( not b in { p where p is Element of P : ( p is Subset of x & p misses y ) } or a = b or a misses b ) ) )

proof

let a be Subset of (x \ y); :: thesis:
assume a in { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then CC: ex a0 being Element of P st
( a = a0 & a0 is Subset of x & a0 misses y ) ;
hence a <> {} ; :: thesis:
for b being Subset of (x \ y) holds
( not b in { p where p is Element of P : ( p is Subset of x & p misses y ) } or a = b or a misses b )

proof

let b be Subset of (x \ y); :: thesis:
assume b in { p where p is Element of P : ( p is Subset of x & p misses y ) } ; :: thesis:
then ex b0 being Element of P st
( b = b0 & b0 is Subset of x & b0 misses y ) ;
hence ( a = b or a misses b ) by CC, EQREL_1:def 4; :: thesis:

end;

hence for b being Subset of (x \ y) holds
( not b in { p where p is Element of P : ( p is Subset of x & p misses y ) } or a = b or a misses b ) ; :: thesis:

end;

hence { p where p is Element of P : ( p is Subset of x & p misses y ) } is a_partition of x \ y by Y1, Y2, EQREL_1:def 4; :: thesis:

end;

hence ex P being finite Subset of B st P is a_partition of x \ y by T1; :: thesis:

end;

hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A by AA, Defdiff2; :: thesis:

end;