for X being set
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