let X be set ; :: thesis: ( ( for A, B being Element of cobool X st not A /\ B is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of A /\ B ) & ( for A, B being Element of cobool X st B c= A holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & ( for A, B being Element of cobool X st not A \ B is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & {X} is countable Subset of (cobool X) & union {X} = X )
set S = cobool X;
A2: ex y being finite Subset of (cobool X) st y is a_partition of X

proof

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: ex y being finite Subset of (cobool X) st y is a_partition of X

then A3: {X} is a_partition of X by EQREL_1:39;
{X} is finite Subset of (cobool X) by ZFMISC_1:7;
hence ex y being finite Subset of (cobool X) st y is a_partition of X by A3; :: thesis: verum

end;

suppose A4: X is empty ; :: thesis: ex y being finite Subset of (cobool X) st y is a_partition of X

{} is finite Subset of {{},{}} by SUBSET_1:1;
hence ex y being finite Subset of (cobool X) st y is a_partition of X by EQREL_1:45, A4; :: thesis: verum

end;

end;

end;

thus for A, B being Element of cobool X st not A /\ B is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of A /\ B :: thesis: ( ( for A, B being Element of cobool X st B c= A holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & ( for A, B being Element of cobool X st not A \ B is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & {X} is countable Subset of (cobool X) & union {X} = X )

proof

let S1, S2 be Element of cobool X; :: thesis: ( not S1 /\ S2 is empty implies ex P being finite Subset of (cobool X) st P is a_partition of S1 /\ S2 )
A7: ( S1 = {} or S1 = X ) by TARSKI:def 2;
( S2 = {} or S2 = X ) by TARSKI:def 2;
hence ( not S1 /\ S2 is empty implies ex P being finite Subset of (cobool X) st P is a_partition of S1 /\ S2 ) by A2, A7; :: thesis: verum

end;

for S1, S2 being Element of cobool X st not S1 \ S2 is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of S1 \ S2

proof

let S1, S2 be Element of cobool X; :: thesis: ( not S1 \ S2 is empty implies ex P being finite Subset of (cobool X) st P is a_partition of S1 \ S2 )
A10: ( S1 = {} or S1 = X ) by TARSKI:def 2;
( S2 = {} or S2 = X ) by TARSKI:def 2;
hence ( not S1 \ S2 is empty implies ex P being finite Subset of (cobool X) st P is a_partition of S1 \ S2 ) by A2, A10, XBOOLE_1:37; :: thesis: verum

end;

hence ( ( for A, B being Element of cobool X st B c= A holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & ( for A, B being Element of cobool X st not A \ B is empty holds
ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & {X} is countable Subset of (cobool X) & union {X} = X ) by ZFMISC_1:7, Lem3; :: thesis: verum