let X be set ; :: thesis:
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis:
A1: for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B by Lem7;
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 by Defdiff2;
let A be Element of S; :: thesis:
let Q be finite Subset of S; :: thesis:
assume that
A3: union Q c= A and
A4: Q is a_partition of union Q ; :: thesis:

per cases ;

suppose A5: S is empty ; :: thesis:

then A6: A is empty by SUBSET_1:def 1;
A7: union Q misses union {} by ZFMISC_1:2;
A8: ( {} is finite Subset of {} & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
Q \/ {} is a_partition of A by A5, A6, EQREL_1:45;
hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A5, A7, A8; :: thesis:

end;

suppose A9: not S is empty ; :: thesis:

per cases ;

suppose A10: A is empty ; :: thesis:

A20: union Q misses union {} by ZFMISC_1:2;
A21: ( {} is finite Subset of S & {} is a_partition of {} ) by XBOOLE_1:2, EQREL_1:45;
Q \/ {} is a_partition of A by A4, A10, A3;
hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A21, A20; :: thesis:

end;

suppose not A is empty ; :: thesis:

hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A1, A2, A3, A4, A9, Lem6; :: thesis:

end;

end;

end;

end;