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: {[x1,x2],[y1,y2]} c= [:{x1,y1},{x2,y2}:]
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in {[x1,x2],[y1,y2]} or [x,y] in [:{x1,y1},{x2,y2}:] )
assume [x,y] in {[x1,x2],[y1,y2]} ; :: thesis: [x,y] in [:{x1,y1},{x2,y2}:]
then ( ( [x,y] = [x1,x2] & x1 in {x1,y1} & x2 in {x2,y2} ) or ( [x,y] = [y1,y2] & y1 in {x1,y1} & y2 in {x2,y2} ) ) by TARSKI:def 2;
hence [x,y] in [:{x1,y1},{x2,y2}:] by ZFMISC_1:87; :: thesis: verum
end;
A2: ( proj1 {[x1,x2],[y1,y2]} = {x1,y1} & proj2 {[x1,x2],[y1,y2]} = {x2,y2} ) by FUNCT_5:13;
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 A2, Th97;
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 ( {x1,y1} in C1 & {x2,y2} in C2 ) by COH_SP:5;
then {[x1,x2],[y1,y2]} in C1 [*] C2 by A1, Th96;
hence [[x1,x2],[y1,y2]] in Web (C1 [*] C2) by COH_SP:5; :: thesis: verum