let X be set ; ( ( 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
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
( ( 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 )
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
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; verum