let C1, C2 be Coherence_Space; :: thesis: 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 ) )
let x1, y1, x2, y2 be set ; :: thesis: ( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )
A1: ( proj1 {[x1,x2],[y1,y2]} = {x1,y1} & proj2 {[x1,x2],[y1,y2]} = {x2,y2} ) by FUNCT_5:16;

hereby :: thesis: ( [x1,y1] in Web C1 & [x2,y2] in Web C2 implies [[x1,x2],[y1,y2]] in Web (C1 [*] C2) )

assume [[x1,x2],[y1,y2]] in Web (C1 [*] C2) ; :: thesis: ( [x1,y1] in Web C1 & [x2,y2] in Web C2 )
then {[x1,x2],[y1,y2]} in C1 [*] C2 by COH_SP:5;
then ( {x1,y1} in C1 & {x2,y2} in C2 ) by A1, Th98;
hence ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) by COH_SP:5; :: thesis: verum

end;

assume ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) ; :: thesis: [[x1,x2],[y1,y2]] in Web (C1 [*] C2)
then A2: ( {x1,y1} in C1 & {x2,y2} in C2 ) by COH_SP:5;
{[x1,x2],[y1,y2]} c= [:{x1,y1},{x2,y2}:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[x1,x2],[y1,y2]} or x in [:{x1,y1},{x2,y2}:] )
assume x in {[x1,x2],[y1,y2]} ; :: thesis: x in [:{x1,y1},{x2,y2}:]
then ( ( x = [x1,x2] & x1 in {x1,y1} & x2 in {x2,y2} ) or ( x = [y1,y2] & y1 in {x1,y1} & y2 in {x2,y2} ) ) by TARSKI:def 2;
hence x in [:{x1,y1},{x2,y2}:] by ZFMISC_1:106; :: thesis: verum

end;

then {[x1,x2],[y1,y2]} in C1 [*] C2 by A2, Th97;
hence [[x1,x2],[y1,y2]] in Web (C1 [*] C2) by COH_SP:5; :: thesis: verum