theorem :: COHSP_1:69

for C being Coherence_Space
for x, y being set holds
( [x,y] in Web ('not' C) iff ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) )