theorem :: COHSP_1:99

for C1, C2 being Coherence_Space
for x1, y1, x2, y2 being set holds
( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )