let X be set ; :: thesis: ( X is c=directed implies not X is empty )
assume for Y being finite Subset of X ex a being set st
( union Y c= a & a in X ) ; :: according to COHSP_1:def 4 :: thesis: not X is empty
then ex a being set st
( union ({} X) c= a & a in X ) ;
hence not X is empty ; :: thesis: verum