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 ) ;
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