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