theorem Th7: :: COH_SP:7

for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )