let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for SM, T being finite Subset of S ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T)
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: for SM, T being finite Subset of S ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T)
let SM, T be finite Subset of S; :: thesis: ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T)
consider RSM being FinSequence such that
A: SM = rng RSM by FINSEQ_1:52;
consider RT being FinSequence such that
B: T = rng RT by FINSEQ_1:52;
C: RSM is FinSequence of S by A, FINSEQ_1:def 4;
RT is FinSequence of S by B, FINSEQ_1:def 4;
then consider P being finite Subset of S such that
D: P is a_partition of (meet (rng RSM)) \ (Union RT) by C, Lem9;
thus ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T) by A, B, D; :: thesis: verum