let X be set ; :: thesis: ( X is c=filtered implies not X is empty )
assume 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 ) ; :: according to COHSP_1:def 5 :: thesis: not X is empty
then ex a being set st
( ( for y being set st y in {} X holds
a c= y ) & a in X ) ;
hence not X is empty ; :: thesis: verum