:: deftheorem defines cap-finite-closed CARDFIL2:def 2 :
for X being non empty set holds
( X is cap-finite-closed iff for SX being non empty finite Subset of X holds meet SX in X );