theorem :: COHSP_1:64

for C1, C2 being Coherence_Space
for x1, x2, y1, y2 being set holds
( [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) iff ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ) )