:: deftheorem defines 'not' COHSP_1:def 21 :
for C being Coherence_Space holds 'not' C = { a where a is Subset of (union C) : for b being Element of C ex x being set st a /\ b c= {x} } ;