:: deftheorem defines c=filtered COHSP_1:def 5 :
for X being set holds
( X is c=filtered iff for Y being finite Subset of X ex a being set st
( ( for y being set st y in Y holds
a c= y ) & a in X ) );