let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for SM being finite Subset of S ex P being finite Subset of S st P is a_partition of meet SM
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for SM being finite Subset of S ex P being finite Subset of S st P is a_partition of meet SM
let SM be finite Subset of S; :: thesis: ex P being finite Subset of S st P is a_partition of meet SM
consider SF being FinSequence such that
A1: rng SF = SM by FINSEQ_1:52;
SF is FinSequence of S by A1, FINSEQ_1:def 4;
hence ex P being finite Subset of S st P is a_partition of meet SM by A1, Lem8; :: thesis: verum