let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for A being Element of S
for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: for A being Element of S
for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
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: for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
let Q be finite Subset of S; :: thesis: ( union Q c= A & Q is a_partition of union Q implies ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) )
assume that
A3: union Q c= A and
A4: Q is a_partition of union Q ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )

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

suppose A5: S is empty ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )

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: verum

end;

suppose A9: not S is empty ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )

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

suppose A10: A is empty ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )

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: verum

end;

suppose not A is empty ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )

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: verum

end;

end;

end;

end;