let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for S1, S2 being Element of S ex P being finite Subset of S st P is a_partition of S1 /\ S2
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for S1, S2 being Element of S ex P being finite Subset of S st P is a_partition of S1 /\ S2
let S1, S2 be Element of S; :: thesis: ex P being finite Subset of S st P is a_partition of S1 /\ S2

per cases ( not S1 /\ S2 is empty or S1 /\ S2 is empty ) ;

suppose not S1 /\ S2 is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of S1 /\ S2

then consider P being finite Subset of S such that
A1: P is a_partition of S1 /\ S2 by Defcap;
thus ex P being finite Subset of S st P is a_partition of S1 /\ S2 by A1; :: thesis: verum

end;

suppose A2: S1 /\ S2 is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of S1 /\ S2

{} is finite Subset of S by SUBSET_1:1;
hence ex P being finite Subset of S st P is a_partition of S1 /\ S2 by A2, EQREL_1:45; :: thesis: verum

end;

end;