:: deftheorem defines CSp COH_SP:def 4 :
for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ;