let C be Coherence_Space; :: thesis: for x being set holds
( x in 'not' C iff ( x c= union C & ( for a being Element of C ex z being set st x /\ a c= {z} ) ) )
let x be set ; :: thesis: ( x in 'not' C iff ( x c= union C & ( for a being Element of C ex z being set st x /\ a c= {z} ) ) )
( x in 'not' C iff ex X being Subset of (union C) st
( x = X & ( for a being Element of C ex z being set st X /\ a c= {z} ) ) ) ;
hence ( x in 'not' C iff ( x c= union C & ( for a being Element of C ex z being set st x /\ a c= {z} ) ) ) ; :: thesis: verum