:: deftheorem Defcap defines cap-finite-partition-closed SRINGS_1:def 1 :
for X being set
for S being Subset-Family of X holds
( S is cap-finite-partition-closed iff for S1, S2 being Element of S st not S1 /\ S2 is empty holds
ex x being finite Subset of S st x is a_partition of S1 /\ S2 );